Astrée automatically proves the absence of runtime errors and invalid con­current behavior in C appli­ca­tions. It is sound for floating-point compu­tations, very fast, and excep­tionally precise. The analyzer also checks for MISRA coding rules and supports quali­fi­cation for ISO 26262, DO-178C level A, and other safety standards. Jenkins and Eclipse plugins are available.

Key Features of Astrée:

  • Astrée is sound: If the analysis does not detect any errors, the absence of runtime errors has been proven. Control and data coverage is 100%.
  • Astrée is precise: Its state-of-the-art analysis engine enables very low false alarm rates.
  • Astrée is scalable: Industrial avionics software with more than 500 KLOC has successfully been analyzed with zero false alarms on a PC in a few hours.
  • Astrée supports precise floating-point arithmetics taking rounding errors into account.
  • False alarms can be safely eliminated by tuning the precision to the software under analysis.
  • Astrée enables you to interactively explore the analysis results.
  • A Qualification Support Kit is available, providing support for automatic tool qualification up to the highest criticality levels.
  • Astrée automatically takes the OS configuration of ARINC653/OSEK/AUTOSAR projects into account.
  • Astrée can be seamlessly integrated with dSPACE TargetLink; dedicated domains ensure unparalleled analysis precision.