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.
6. Publications
J. Bertrane,
F. Camporesi,
P. Cousot,
R. Cousot,
J. Feret,
V. Laviron,
A. Miné,
X. Rival,
A. Romanel,
M. Zanioli.
