Semantics and Abstract Interpretation
Scientific leader: Patrick Cousot
En Français / In French
-
The production of reliable and efficient software requires, at least
in part, the automatization of its construction. To reach this objective,
it is indispensable to study programs and their executions as mathematical
objects.
- We take a semantic (1) point of view, in order
to define the nature of the program computations and the rigorous
deductive reasonings that can be applied to prove their run-time
properties.
- We also take the computational point of view of
abstract interpretation (2):
programs can be the object of computer manipulation in order
to automatically discover their semantic properties. These
programs for manipulating programs can themselves be the object
of formal study and their design may be automatized, which are
the purpose of our work on program static analysis by abstract
interpretation.
-
Our various research themes are about:
- The semantics of programming languages:
- models of sequential, parallel, distributed, real time, probabilistic,
... computations;
- methods for defining the semantics of programming languages and
more generally, specifying computer systems;
- study of the correspondences between semantics;
- methods for proving semantic properties of programs;
- study of the correctness and completeness of these proof methods with
respect to a semantics;
- etc.
- Program static analysis by abstract interpretation:
- discrete approximation techniques for abstracting computation domains
and their use for approximating semantics;
- discrete mathematical structures in order to express approximate
semantical properties of objects manipulated by programs (like, for example,
linear (in)equality or congruence relationships among numerical values
or aliasing and sharing properties among linked data structures);
- type systems, type verification and inference;
- abstract interpretation of program control structures (higher-order
functions in functional languages, backtracking in logic languages,
communication and synchronization mechanisms in parallel languages, etc);
- iterative and approximated resolution of fixpoint systems of equations
on posets, in particular by simplification and convergence acceleration;
- etc.
- The considered applications are:
- (static) debugging tools;
- automatized test generation;
- compile-time optimization;
- program transformation for vectorial, massively parallel or
distributed machines;
- program verification tools (provers, model-checkers, etc.);
for imperative, functional, logic, parallel, object-oriented, ... programs.
- A bibliography on abstract interpretation.
(1) The semantics of a program describes the run-time behaviors
of this program that is the set of possible computations as a function of
the input data or interaction with the environment, whether these
computations do not terminate or terminate by the production of one or several
correct or erroneous results.
(2) Program analysis by Abstract interpretation is the
static (without execution) and automatic (without human interaction)
of dynamic (during run-time) program properties. Formally,
abstract interpretation relies on an idea of discrete approximation
which consists in replacing the reasoning on a concrete
exact semantics by a computation on an abstract approximate semantics.
The uncertainty resulting from the approximation does not concern
the inaccuracy of the properties which are automatically inferred
but the existence of uncomputable properties for which the
answer `` I don't know'' is possible. The rule of signs in a
commutative ring (such as ``minus times minus is plus'') is a trivial example of abstract interpretation.