What is the Astrée Static Analyzer?

Updated

Astrée is a static program analyzer designed to prove the absence of run-time errors (RTE) in programs written in the C programming language. It is developed by the Centre National de la Recherche Scientifique (CNRS), the École Normale Supérieure (ENS), and INRIA (since September 2007), with Patrick Cousot as project leader. The name stands for Analyseur statique de logiciels temps-réel embarqués (real-time embedded software static analyzer). It is most relevant if you work with synchronous, time-triggered, safety-critical embedded software written or automatically generated in C.

What Astrée does

Astrée analyzes structured C programs that may have complex memory usage, but it targets programs without dynamic memory allocation and recursion. Its core objective is to prove that no run-time errors can occur — not merely to find some bugs, but to establish the absence of RTE across the analyzed program.

This focus makes it suited to embedded domains such as:

  • Earth transportation
  • Nuclear energy
  • Medical instrumentation
  • Aeronautic and aerospace applications
  • Synchronous control/command systems, including electric flight control and space vessel maneuvers

Proven industrial results

Astrée's main applications appeared two years after the project started. Since then it has produced notable results on static analysis of synchronous, time-triggered, real-time, safety-critical embedded software:

Milestone Detail
Nov. 2003 Proved completely automatically the absence of any RTE in the primary flight control software of the Airbus A340 fly-by-wire system
Program size 132,000 lines of C
Analysis time 1 h 20 on a 2.8 GHz 32-bit PC using 300 Mb of memory; 50 min on a 64-bit AMD Athlon 64 using 580 Mb
From Jan. 2004 Extended to analyze the electric flight control codes then in development and test for the A380 series

Development and background

The development of Astrée started from scratch in November 2001 at the Laboratoire d'Informatique of the École Normale Supérieure (LIENS). It was initially supported by the ASTRÉE project, CNRS, and ENS, and since September 2007 by INRIA (Paris—Rocquencourt).

Participants listed include Patrick Cousot (project leader), Radhia Cousot, Jérôme Feret, Antoine Miné, and Xavier Rival. Former participants include Bruno Blanchet (Nov. 2001 — Nov. 2003), David Monniaux (Nov. 2001 — Aug. 2007), and Laurent Mauborgne (Nov. 2001 — Aug. 2010).

When Astrée is a fit

Astrée is aimed at proving run-time properties of C programs under specific constraints. It is a strong match when your code is:

  • Written in C
  • Structured, with no dynamic memory allocation and no recursion
  • Embedded, real-time, and safety-critical
  • Synchronous or time-triggered in nature

If your program relies on dynamic memory allocation or recursion, Astrée's documented scope does not cover it. For licensing and exploitation details, the site provides a dedicated "Exploitation license of Astrée" section, and further technical depth is available under "Theoretical Background of Astrée" and "Which Program Run-Time Properties are Proved by Astrée?".