ASTRÉE is a sound parametric static analyzer that proves the absence of runtime errors and data races.
It reports program defects caused by unspecified and undefined behaviours according to the C/C++ language standards, program defects caused by invalid concurrent behaviour, and computes program properties relevant for functional safety.
Zero false negatives & false positives
Lower false negatives mean more confidence the analysis has not missed problems. Lower false positives mean less wasted effort on assessing and discarding as ‘false’ a reported violation (alarm).
Sound data & control flow coupling
ASTRÉE computes data and control flow reports containing a detailed listing of accesses to global and static variables sorted by functions or variables, and caller/callee relationships between functions.
Error classes reported
ASTRÉE is sound for floating-point computations and handles them precisely and safely. It takes all potential rounding errors into account.