ENS CNRS INRIA

École Normale Supérieure
Computer Science Department
Abstract interpretation and semantics    fran\347ais


1. Members

2. Project/team ABSTRACTION

3. Research Interests

The group works on semantics and abstract interpretation, a research domain that it pioneered. The main practical applications are related to static analysis.
Semantics
In computer science, the formal semantics of a language provides, for all programs written in this language, a mathematical model of all possible behaviors of a computer system executing this program, in interaction with any possible environment. All interesting questions about a program semantics are undecidable. This means than no computer can always answer these questions in a finite time.
Abstract Interpretation
Abstract interpretation is a theory of the approximation of semantics of (programming or specification) languages. It formalizes the idea that the semantics can be more or less precise according to the considered level of observation. If the approximation is coarse enough, the abstraction of a semantics yields a less precise but computable version. Because of the corresponding loss of information, not all questions can be answered, but all answers given by the effective computation of the approximate semantics are always correct. The informal presentation Abstract Interpretation in a Nutshell aims at providing a short intuitive introduction to the theory.
Static Analysis
Static analysis uses abstract interpretation to derive a computable semantics from the standard semantics. Therefore computers can analyze the run-time behavior of programs and software at compile-time, that is before and without execution. This is essential, for example in critical computer systems (planes, launchers, nuclear plants) so that bugs (which sometime escape to the perspicacity of programmers) can be detected before producing catastrophes!

4. Software

ASTRÉE is an example of static analyzer able to verify the absence of run-time errors for synchronous control/command C programs while ASTRÉEA is under development for asynchronous programs.

5. Seminar « Semantics and Abstract Interpretation (SIA) »

6. Publications

J. Bertrane, F. Camporesi, P. Cousot, R. Cousot, J. Feret, V. Laviron, A. Miné, X. Rival, A. Romanel, M. Zanioli.
Last modified: Tuesday, 26-Apr-2011 14:37:19 CEST