Astrée is a static program analyzer that proves the absence of run-time errors (RTE) in safety-critical embedded applications written or automatically generated in C.

Astrée screenshot
Astrée screenshot

Astrée analyzes structured C programs with complex memory usages, but without recursion or dynamic memory allocation. This targets embedded applications as found in earth trans­por­tation, nuclear energy, medical instrumentation, aeronautics and space flight, in particular syn­chro­nous control/command such as electric flight control.

Which run-time properties are analyzed by Astrée?

Astrée analyses whether the C programming language is used correctly and whether there can be any run-time errors during any execution in any environment. This covers:

  • Any use of C that has undefined behavior according to ISO/IEC 9899:1999, the international norm governing the C program­ming language. Examples include division by zero or out-of-bounds array indexing.
  • Any use of C that violates hardware-specific aspects as defined by ISO/IEC 9899:1999, e.g. the size of integers and arithmetic overflow.
  • Any potentially harmful or incorrect use of C that violates user-defined programming guide­lines, such as no modular arithmetic for integers (even if this might be the hardware choice).
  • Any violation of optional user-defined assertions to prove additional run-time properties (simi­lar to assert diagnostics).

Astrée can be customized and integrated into established tool-chains.