Astrée comes with comprehensive documentation and lots of real-world examples.
Sample analysis results.
The call graph browser provides an overview of the alarm distribution in the analyzed software.
When creating a new project, a wizard dialog guides you through the basic analysis settings. It also provides online help for each of the configured options.
As of release 10.12, 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.