Astrée (static analysis)
Astrée ("Analyseur statique de logiciels temps-réel embarqués") is a static analyzer based on abstract interpretation. It analyzes programs written in the programming languages C and C++, and emits 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. It is proprietary software written in the language OCaml.
| Original author(s) | Patrick Cousot, Radhia Cousot, Jérôme Feret, Antoine Miné, Xavier Rival |
|---|---|
| Developer(s) | Laboratoire d'Informatique, École normale supérieure (Paris) (LIENS) French Institute for Research in Computer Science and Automation (INRIA, Paris–Rocquencourt) |
| Initial release | 16 December 2002 |
| Stable release | 23.10
/ 2023 |
| Written in | OCaml |
| Operating system | Windows 10, Linux 64-bit, macOS |
| Platform | x86-64; AArch64 (M1, M2, M3) |
| Available in | English |
| Type | static analyzer |
| License | Proprietary |
| Website | www |
The tool is tailored toward 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 added operating system (OS) specifications. On multi-core processors, the placement of threads to cores, and the use of mutex locks and spinlocks are analyzed.
Astrée was developed in Patrick Cousot's group at École Normale Supérieure, a joint group with CNRS, and is available commercial from AbsInt GmbH. It is used in the defense–aerospace, industrial control, electronic, and automotive industries. One of the main industrial users is Airbus.