Astrée ("Analyseur statique de logiciels temps-réel embarqués"[1]) is a static analyzer based on abstract interpretation.
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 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.
Astrée supports the ARINC 653, OSEK, and AUTOSAR execution models and can be adapted to added operating system (OS) specifications.