Astrée is a static code analyzer that proves the absence of run­time errors and invalid con­current behavior in safety-critical software written or gen­er­ated in C or C++.

▪ Sound static Analyzer based on Abstract Interpretation designed to prove the absence of runtime
errors and data races in C programs
(C99 standard)
▪ If Astrée does not report any alarm (potential runtime error / data race) this is a formal proof that there
are no such errors in the code.
▪ Reference customer: Airbus flight control software (DO-178B level A). No false alarm on >755.000
LOC, analysis time 6h.
▪ Automatic tool qualification according to ISO-26262, DO-178B/DO-178C, IEC-61508, IEC-60880, etc.
by Qualification Support Kits (QSK) and Qualification Software Life Cycle Data reports (QSLCD).
▪ Support for model-based code generation; tool couplings to dSPACE TargetLink, model link to
MATLAB/ SIMULINK available.
▪ Open formats, full continuous verification support.