Astrée Sound Software Scanner

Astrée is a parametric static analyser designed to prove the absence of runtime errors and data races in software programs written in C. Astrée is parameterisable and can be adapted to the specific software being analysed.  This is one of the key features to assure an extremely high analysis precision.

The Challenge

Runtime errors and data races can provoke erroneous program behaviour and may even cause the software to crash. Traditional static software analysis and testing can be used to detect errors but not to prove their absence. Astrée’s static analysis engine is based on abstract interpretation. The methodology is used to prove the absence of runtime errors and data races.

Examples of Software Errors detected by Astrée:

  • Out-of-bound array accesses
  • Erroneous pointer manipulations and dereferencing (NULL, uninitialized and dangling pointers)
  • Integer and floating-point divisions by zero
  • Integer and floating-point arithmetic overflows
  • Read accesses to uninitialized variables
  • Violations of user-specified assertions
  • Data races between concurrent threads
  • Inconsistent locking

Astrée also reports accesses to shared variables, non-terminating loops, unreachable code, violations of MISRA rules, and violations of CERT-C and CWE rules to prevent potential security risks.

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 analysed with zero false alarms on a PC in a few hours.
  • Astrée supports precise floating-point arithmetic’s 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.