Astrée Static Analyzer
An abstract-interpretation-based static analyzer designed to prove absence of selected run-time errors in defined classes of critical C software.
Technical Context
Astrée is an abstract-interpretation-based analyzer developed for real-time and safety-critical embedded C. Its objective is property-specific proof under a defined program model, rather than only heuristic bug finding.
The analysis combines numerical abstract domains, fixed-point computation and convergence techniques. Sound over-approximation aims not to miss relevant failures while allowing false alarms.
Boundaries
The guarantee depends on supported C features and environment assumptions. The official Astrée description defines restrictions for the targeted program class, including the absence of recursion and dynamic memory allocation.