STATIC PROGRAM ANALYSIS

Static progvram analysis aims at determining properties of the behaviour of a program without actually executing it. Static analysis is founded on the theory of abstract interpretation for proving the correctness of analyses with respect to the semantics of a programming language.  An analysis can often be divided into two phases:
  1. A first phase in which a program is translated into a system of equations or constraints over a partial order of program properties. The solutions to the system represent correct information about the particular property analysed for. The partial order reflects the relative precision of the solutions. 
  2. A second resolution phase in which an actual solution is calculated. This phase can rely either on general iterative work-set algorithms or on more domain-specific symbolic resolution techniques. 
The first phase depends a) on the programming language used for writing the programs being analysed and b) on the kind of property analysed for. The second phase is largely independent of the actual analysis and can rely on general solvers that can serve as back-end of several analysers.

My work has been concerned with

Types in program analysis

Non-standard type systems can be a convenient way of specifying a static analysis but beg the question of how they relate to other ways of writing analyses, in particular abstract interpretation. It turns out that intersection type systems are useful for setting up a relation between these two worlds because intersection types can encode the lattices used in abstract interpretation (notably lattices of functions). This resuilt (that was first reported at FPCA'91) has since then undergone several extension. A rich set of data types can be accommodated. Combining intersection types with parametric polymorphism yields more modular analyses.
   A recent survey appeared in the Neil Jones Festschrift in 2002. See also the web page maintained by Jens Palsberg on type-based program analysis.

Functional, synchronous, OO,...

I've been involved in analysis activities for several language paradigms, including:
  • analysing memory consumption in functional languages
  • extending analyses from monomorphic to polymorphic languages 
  • finding clocks and relational dataflow information in synchronous languages 
  • control-flow analysis ...

Some of these analyses serve mainly optimisation purpose. Others are used to perform program verification, as for example the control flow analysis for verifying security properties of Java programs.

Control-flow analysis

Control-flow analysis serves to build a control-flow graph for programs for which the flow of control cannot be determined directly from the program syntax. This includes higher-order functional langauges (where the goal is to determine the set of functions to which the expression e1can evaluate to in an application (e1 e2)) and object oriented languages where virtual method calls such as X.m() will invoke different methods according to the objects stored in X.
   With A. Banerjee, I've written an article in Mathematical Structures in Computer Science showing how ranked intersection types provide for modular control flow analysis of a higher-order functional language.
   With F. Spoto, we had a paper in FoSSaCS 2001 (with an extended versioon to appear in ACM TOPLAS) where we investigated the foundations of class analysis for OO languages, using abstract interpretation to classify and compare various existing analyses.