14
Key Facts
- Astrée finds all runtime errors – guaranteed.
- No miscompilation with CompCert – guaranteed.
- Astrée: market-leading static analysis for safety and security.
Categories
Test and Verification Software Methods and Tools for Secure Embedded Systems Static and Run-Time Analysis Tools Other Tools and Software
Product information
- Astrée is a static program analyzer that proves the absence of run-time errors in safety-critical C/C++ code (incl. data races, division by zero, out-of-bounds array accesses, erroneous pointer manipulation, and arithmetic overflows). It contributes to demonstrating freedom of interference, computes code metrics, and verifies compliance with MISRA C/C++, SEI CERT C/C++, and other coding standards. More info at https://www.absint.com/astree/index.htm.
- CompCert is a formally verified optimizing C compiler. The level of confidence in the correctness of the compilation process is unprecedented and helps meet the highest standards of software assurance. More info at https://www.absint.com/compcert/index.htm.
Download
Watch our product video
Source level analysis and compilation: Astrée and CompCert Video