Astrée Run-Time Error Analyzer

Beschreibung

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.