The Antique CNRS/ENS/INRIA Team carries out research in semantics, static analysis, abstract interpretation of programs and biological systems.
We search for automatic techniques to compute semantic properties of programs (in particular safety critical embedded programs) and biological systems.
Properties of interest include, among others, safety (such as absence of runtime errors, preservation of data invariants), liveness (such as termination), security (absence of information leak).
Such properties are usually not computable, or can only be computed at a prohibitive cost in the case of finite systems.
Therefore we tackle them with techniques based on conservative abstraction.
Members of the group
Head of the team
Ongoing or recent projects and tools
- Anastasec: verification of security properties in safety critical embedded softwares
- Apron: a library of numerical abstract domains
- Astrée: a static analyzer for large synchronous safety critical programs
- AstréeA: a static analyzer for large asynchronous safety critical programs
- Big Mechanism
- CwC: Communicating with Computers
- http://www.kappalanguage.org/: a rule-based language for modeling protein interaction networks
- MemCAD: a library of composite memory abstract domains
- Verasco: verification of static analyzers and compilers