Astrée screenshots

Astrée screenshot

Astrée comes with comprehensive documentation and a variety of real-world examples.


Astrée screenshot

When creating a new project, Astrée guides you through the analysis settings and offers interactive help for each of the configured options.


Astrée screenshot

It is possible to specify a list of original source files and preprocessor settings (include paths and defines). The specified files can be automatically preprocessed and analyzed by Astrée using a built-in preprocessor.


Astrée screenshot

Sample analysis results. Several runtime errors have been found and can be interactively explored, commented on, or fixed right away in the built-in editor.

The errors are classified by severity, and the overall result is summed up by a traffic-lights symbol.

The results can be exported, for example as customizable HTML reports, for documentation and certification purposes. The entire project can be saved as well, including all files, settings, annotations and comments.


Astrée screenshot

Code parts that cause the runtime errors are highlighted in the built-in text editor and can be fixed right there.


Astrée screenshot

The call graph browser provides an overview of the alarm distribution in the analyzed software.


Astrée screenshot

With the seamlessly integrated RuleChecker, you can check your code for adherence to standards such as MISRA, CWE, ISO/IEC, and SEI CERT C, compute code metrics such as com­ment den­sity or cyclomatic complexity, and check metric thresholds.