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 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.