Astrée (static analysis)

Astrée ("Analyseur statique de logiciels temps-réel embarqués"[1]) is a static analyzer based on abstract interpretation. It analyzes programs written in the C programming language and outputs an exhaustive list of possible runtime errors and assertion violations. The defect classes covered include divisions by zero, buffer overflows, dereferences of null or dangling pointers, data races, deadlocks, etc. Astrée includes a static taint checker and helps finding cybersecurity vulnerabilities, such as Spectre.

The tool is tailored towards safety-critical embedded code: specific analysis techniques are used for common control theory constructs (finite state machines, digital filters, rate limiters...) and floating-point numbers.

Concurrent code is analyzed with a sound interleaving semantics that is aware of the concurrent threads of execution, their priorities and synchronization mechanisms. Astrée supports the ARINC 653, OSEK and AUTOSAR execution models and can be adapted to additional OS specifications. On multi-core processors the placement of threads to cores, and the usage of mutex locks and spinlocks are taken into account.

Astrée was developed in Patrick Cousot's group at École Normale Supérieure, a joint group with CNRS, and is marketed by AbsInt GmbH. It is used in the defense/aerospace, industrial control, electronic, and automotive industries. One of the main industrial users is Airbus.[2]

Astrée is a commercial product available from AbsInt Angewandte Informatik.