http://www.absint.de/astree/

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.

  1. [2010/06/04] [Video] Beautiful Code and Programming Discipline by Certifiedtest (1310)
  2. [2010/05/28] [Free] StyleCop : Static code analysis tool for C# (Microsoft) by Googler ()
  3. [2011/03/29] [Ebook] Embedded C *2 by @lionking (2223)
  4. [2010/05/27] [Paid] Vigilant Sentry : a static code analyzer for C/C++ *1 by NumLock ()
  5. [2010/05/28] [Paid] Ada-ASSURED : Testing and reviewing for coding style by Googler ()