Proven Absence of Runtime Errors with Sound Static Analysis
Astrée is a sound parametric static analyzer that proves the absence of runtime errors and data races.
Astrée proves the absence of errors. It reports program defects caused by unspecified and undefined behaviours according to the C and 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.
HOW ASTRÉE FITS IN YOUR VERIFICATION PROCESS
QA Systems static analysis and software testing tools support verification in the linear flow of software development below. We recommend applying sequential approach to these verification stages with tools that are designed and targeted for each purpose.
- COMPLY > Use QA-MISRA for fast coding standard compliance at the developer’s desktop first.
- TEST > Use Cantata for automated dynamic execution of the standard compliant software.
- ANALYZE > Use Astrée for proving absence of run-time errors on whole application.
NB: Astrée uses the same configuration as QA-MISRA, so the effort to apply it later to a QA-MISRA project later is low.
For Astrée we provide a Qualification Support Kit (QSK) which automatically executes a full tool qualification verification test suite on the installed tool configuration and generates the necessary reports for tool qualification