ABSTRACTION Research team

Abstract Interpretation and Static Analysis

Team presentation

Scientific problematic
An error in a critical software may have catastrophic human or economic consequences, in particular for embedded systems. It is therefore particularly important to check that such software is safe and secure, before operational exploitation. ABSTRACTION develops abstract interpretation techniques for effectively computing an over-approximation of the possible runtime behaviors of the analyzed programs. Static analysis by abstract interpretation scales up on industrial codes. It is safe (in case of success, the analyzed software is definitely proved correct) but incomplete (in some cases the proof search may fail because of undecidability problems and lead to false alarms). By specializing the analysis to well-defined families of programs, it is possible to eliminate false alarms.

In this context, the objectives of ABSTRACTION consist in:

  • Formalizing semantic models of the programs and properties to be proved;
  • Developing suitable abstractions, allowing for a rapid and precise computation, that is allowing the effective proof of the required properties;
  • Implementing these static analyses and apply them to industrial codes;
  • Favoring the industrialization of static analysis techniques in the mid-term.

The present research themes are more specifically related to the precise static analysis of synchronous, quasi-synchronous and asynchronous software, of biological systems, and of cryptographic protocols.

Software
• ASTRÉE: static analyzer for proving the absence of runtime errors in safety critical synchronous control/command avionic software written in C.
• ProVerif and CryptoVerif: tools for proving the security of cryptographic protocols.

Milestone
ASTRÉE is currently used to the verification of absence of runtime errors in safety critical synchronous electric flight control avionic software.

International and industrial relations

  • Contracts: European projects, ANR, ACI, RNTL, and industrial contracts.
  • Industrial collaborations: Airbus France, Astrium Transportation, Esterel technologies, etc.
  • Academic collaborations: Universities of Berkeley, Harward, Verona, École Polytechnique, École Normale Supérieure of Cachan.
  • Teaching: École Normale Supérieure, École Polytechnique, Parisian Research Master in Computer Science.

Keywords: Abstract interpretation Abstract models Abstraction Certification Cryptographic protocols Embedded systems Proofs Semantics Software Static analysis Verification Safety Security. Design an

Research teams of the same theme :

Inria Headquarters and research centres

Direct links

Social