The Astrée Static Analyzer


CNRS Centre National de la Recherche Scientifique ENS École Normale Supérieure ENS INRIA (since Sep. 2007)

Participants:

Patrick Cousot (project leader), Radhia Cousot, Jérôme Feret, Antoine Miné, Xavier Rival

Former participants:

Bruno Blanchet (Nov. 2001 — Nov. 2003), David Monniaux (Nov. 2001 — Aug. 2007), Laurent Mauborgne (Nov. 2001 — Aug. 2010).

Contact(‡):  electronic contact to Astrée

Astrée stands for Analyseur statique de logiciels temps-el embarqués (real-time embedded software static analyzer). The development of Astrée started from scratch in Nov. 2001 at the Laboratoire d'Informatique of the École Normale Supérieure (LIENS), initially supported by the ASTRÉE project, the Centre National de la Recherche Scientifique, the École Normale Supérieure and, since September 2007, by INRIA (Paris—Rocquencourt).

Objectives of Astrée

Astrée is a static program analyzer aiming at proving the absence of Run Time Errors (RTE) in programs written in the C programming language. On personal computers, such errors, commonly found in programs, usually result in unpleasant error messages and the termination of the application, and sometimes in a system crash. In embedded applications, such errors may have graver consequences.

Astrée analyzes structured C programs, with complex memory usages, but without dynamic memory allocation and recursion. This encompasses many embedded programs as found in earth transportation, nuclear energy, medical instrumentation, aeronautic, and aerospace applications, in particular synchronous control/command such as electric flight control [30], [31] or space vessels maneuvers [32].

Industrial Applications of Astrée

The main applications of Astrée appeared two years after starting the project. Since then, Astrée has achieved the following unprecedented results on the static analysis of synchronous, time-triggered, real-time, safety critical, embedded software written or automatically generated in the C programming language:

  • In Nov. 2003, Astrée was able to prove completely automatically the absence of any RTE in the primary flight control software of the Airbus A340 fly-by-wire system, a program of 132,000 lines of C analyzed in 1h20 on a 2.8 GHz 32-bit PC using 300 Mb of memory (and 50mn on a 64-bit AMD Athlon™ 64 using 580 Mb of memory).
      A340-300
 
  • From Jan. 2004 on, Astrée was extended to analyze the electric flight control codes then in development and test for the A380 series. The operational application by Airbus France at the end of 2004 was just in time before the A380 maiden flight on Wednesday, 27 April, 2005.
      A380
 
      ESA-ATV

Exploitation license of Astrée

Starting Dec. 2009, Astrée is available from AbsInt Angewandte Informatik   AbsInt (www.absint.de/astree/).

Theoretical Background of Astrée

The design of Astrée is based on abstract interpretation, a formal theory of discrete approximation applied to the semantics of the C programming language. The informal presentation Abstract Interpretation in a Nutshell aims at providing a short intuitive introduction to the theory. A video introduces program verification by abstract interpretation (in French: « La vérification des programmes par interprétation abstraite »  fran\347ais). More advanced introductory references are [1], [2] and [3].

Briefly, program verification — including finding possible run-time errors — is undecidable: there's is no mechanical method that can always answer truthfully whether programs may or not exhibit runtime properties — including absence of any run-time error —. This is a deep mathematical result dating from the works of Church, Gödel and Turing in the 1930's. When faced with this mathematical impossibility, the choice has been to design an abstract interpretation-based static analyzer that will automatically:

Of course, the goal is to be precise, that is to minimize the number of false alarms. The analysis must also be cost-effective, e.g. being a small fraction of the costs of running all tests of the program. In the context of safety-critical reactive software, the goal of zero false alarm was first attained when proving the absence of any RTE in the primary flight control software of the Airbus A340.

Astrée is based on the theory of abstract interpretation [1,2,3] and so proceeds by effectively computing an overapproximation of the trace semantic properties of analyzed programs and then proving that these abstract properties imply the absence of runtime errors. The program analysis is iterative [5], structural [10] (by induction on the program syntax), interprocedural and context-sensitive for procedures [6], and extremely precise for memory [24]. It combines several abstractions of a trace semantics [7,19] with a weak form of reduced product [7,26]. The basic general-purpose abstractions are either non-relationals (like intervals [4,5])) or weakly relational (like octagons [16]) with uniform interfaces [23]. Astrée precision comes from a clever handling of disjuctions [12,14,19] and domain-specific abstract domains [13,17] for control/command. Most abstractions are infinitary which requires convergence acceleration with widening/narrowing [5,9]. The soundness of the abstractions is based on Galois connections [5,7] or concretization-based [8] in absence of best abstraction.

Which Program Run-Time Properties are Proved by Astrée?

Astrée aims at proving that the C programming language is correctly used and that there can be no Run-Time Errors (RTE) during any execution in any environment. This covers: Astrée is parameterized so as to be adaptable to the end-user verification needs.

Three Simple Examples ... Hard to Analyze in the Large

The examples below show typical difficulties in statically analyzing control/command programs. Of course, the real difficulty is to scale up!

Booleans

Control/command programs, in particular synchronous ones, manipulate thousands of boolean variables. Analyzing which program run-time properties hold when each such boolean variable is either true or false rapidly leads to a combinatorial explosion of the number of cases to be considered, that is prohibitive time and memory analysis costs.

For example, the analysis of the following program by Astrée:

/* boolean.c */
typedef enum {FALSE = 0, TRUE = 1} BOOLEAN;
BOOLEAN B;
void main () {
  unsigned int X, Y;
  while (1) {
    /* ... */
    B = (X == 0);
    /* ... */
    if (!B) {
      Y = 1 / X;
    };
    /* ... */
  };
}
yields no warning (thanks to the relationskip automatically determined between B and X), thus proving the absence of any run-time error (integer divide-by-zero can never happen when executing this program).

Astrée has shown to be able to handle successfully thousands of boolean variables, with just enough precision to avoid both false alarms and combinatorial explosion [12].

Floating point computations

Command programs controlling complex physical systems are derived from mathematical models designed with real numbers whereas computer programs perform floating point computations. The two computation models are completely different and this can yield very surprising results, such as:

/* float-error.c */
int main () {
    float x, y, z, r;
    x = 1.000000019e+38;
    y = x + 1.0e21;
    z = x - 1.0e21;
    r = y - z;
    printf("%f\n", r);
}
% gcc float-error.c
% ./a.out
0.000000
% 
/* double-error.c */
int main () {
  double x; float y, z, r;
  /* x = ldexp(1.,50)+ldexp(1.,26); */
  x = 1125899973951488.0; 
  y = x + 1;
  z = x - 1;
  r = y - z;
  printf("%f\n", r);
}
% gcc double-error.c
% ./a.out
134217728.000000
% 

which could have been thought to print respectively 2.0e21 and 2.0 (based on the reasoning that (x+a)-(x-a) = 2a, which is erroneous because of roundings)!

Astrée handles floating point computations precisely and safely. For example, Astrée proves the following program free of run-time error (but for a "Loop never terminates" warning) when running on a machine with floats on 32 bits:

/* float.c */
void main () {
    float x,y,z;
    if ( (((*((unsigned*)&x) & 0x7f800000) >> 23) != 255 ) /* not NaN */
       && (x >= -1.0e38) && (x <= 1.0e38) ) {
        while (1) {
            y = x+1.0e21;
            z = x-1.0e21;
            x = y-z;
        }} 
    else
        return;
}
Astrée is sound for floating point computations in that it takes all possible rounding errors into account (and there might be cumulative effects in programs computing for hours) [12,13].

Digital filters

Control/command programs perform lots of digital filtering, as shown by the following example:

/* filter.c */
typedef enum {FALSE = 0, TRUE = 1} BOOLEAN;
BOOLEAN INIT;
float P, X;

void filter () {
  static float E[2], S[2];
  if (INIT) {
      S[0] = X;
      P = X;
      E[0] = X;
  } else { 
      P = (((((0.5 * X) - (E[0] * 0.7)) + (E[1] * 0.4)) + (S[0] * 1.5)) - (S[1] * 0.7));
  }
  E[1] = E[0];
  E[0] = X;
  S[1] = S[0];
  S[0] = P;
}

void main () {
  X = 0.2 * X + 5;
  INIT = TRUE;
  while (1) { 
    X = 0.9 * X + 35;
    filter ();
    INIT = FALSE;
  }
}

The absence of overflow (and more precisely that P is in [-1327.05, 1327.05] as found by Astrée) is not obvious, in particular because of 32/64 bits floating point computations. The situation is even more inextricable in the presence of boolean control, cascades of filters, etc.

Astrée knows enough about control theory to make precise analyzes of filters [12,13].

Astrée is sound, automatic, efficient, domain-aware, parametric, modular, extensible and precise

Rapid overviews of Astrée is proposed in [14] and [18].

Presentations of Astrée

Astrée Flyer

Introductory Bibliographic References on Abstract Interpretation

  1. Patrick Cousot.
    Interprétation abstraite.
    Technique et Science Informatique, Vol. 19, Nb 1-2-3. Janvier 2000, Hermès, Paris, France. pp. 155—164. (French)

  2. Patrick Cousot.
    Abstract Interpretation Based Formal Methods and Future Challenges.
    In Informatics, 10 Years Back - 10 Years Ahead, R. Wilhelm (Ed.), Lecture Notes in Computer Science 2000, pp. 138—156, 2001.
  3. Patrick Cousot & Radhia Cousot.
    Basic Concepts of Abstract Interpretation.
    In Building the Information Society, R. Jacquard (Ed.), Kluwer Academic Publishers, pp. 359—366, 2004.

Abstract Interpretation foundations of Astrée

  1. Patrick Cousot & Radhia Cousot.
    Static Determination of Dynamic Properties of Programs.
    In Proceedings of the second international symposium on Programming, B. Robinet (Ed), Paris, France, pages 106—130, 13—15 April 1976, Dunod, Paris.
  2. Patrick Cousot & Radhia Cousot.
    Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints.
    In Conference Record of the Sixth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 238—252, Los Angeles, California, 1977. ACM Press, New York.
  3. Patrick Cousot & Radhia Cousot.
    Static determination of dynamic properties of recursive procedures.
    In IFIP Conference on Formal Description of Programming Concepts, E.J. Neuhold, (Ed.), pages 237—277, St-Andrews, N.B., Canada, 1977. North-Holland Publishing Company (1978).
  4. Patrick Cousot & Radhia Cousot.
    Systematic Design of Program Analysis Frameworks.
    In Conference Record of the Sixth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 269—282, San Antonio, Texas, 1979. ACM Press, New York.
  5. Patrick Cousot & Radhia Cousot.
    Abstract interpretation frameworks.
    Journal of Logic and Computation, 2(4):511—547, August 1992.
  6. Patrick Cousot & Radhia Cousot.
    Comparing the Galois connection and widening/narrowing approaches to abstract interpretation.
    Programming Language Implementation and Logic Programming, Proceedings of the Fourth International Symposium, PLILP'92, Leuven, Belgium, 13—17 August 1992, Volume 631 of Lecture Notes in Computer Science, pages 269—295. © Springer-Verlag, Berlin, Germany, 1992.
  7. Patrick Cousot.
    The Calculational Design of a Generic Abstract Interpreter.
    In Broy, M., and Steinbrüggen, R. (eds.): Calculational System Design. NATO ASI Series F. Amsterdam: IOS Press, 1999.

Bibliographic References on Astrée

  1. Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux & Xavier Rival.
    Design and Implementation of a Special-Purpose Static Program Analyzer for Safety-Critical Real-Time Embedded Software, invited chapter.
    In The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones, T. Mogensen and D.A. Schmidt and I.H. Sudborough (Editors). Volume 2566 of Lecture Notes in Computer Science, pp. 85—108, © Springer.
  2. Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, & Xavier Rival.
    A Static Analyzer for Large Safety-Critical Software.
    In PLDI 2003 — ACM SIGPLAN SIGSOFT Conference on Programming Language Design and Implementation, 2003 Federated Computing Research Conference, June 7—14, 2003, San Diego, California, USA, pp. 196—207, © ACM.
  3. Jérôme Feret.
    Static analysis of digital filters.
    In ESOP 2004 — European Symposium on Programming, D. Schmidt (editor), Mar. 27 —Apr. 4, 2004, Barcelona, ES, Volume 2986 of Lecture Notes in Computer Science, pp. 33—48, © Springer.
  4. Laurent Mauborgne.
    Astrée: verification of absence of run-time error.
    In Building the Information Society, R. Jacquard (Ed.), Kluwer Academic Publishers, pp. 385—392, 2004.
  5. Antoine Miné.
    Relational abstract domains for the detection of floating-point run-time errors.
    In ESOP 2004 — European Symposium on Programming, D. Schmidt (editor), Mar. 27 — Apr. 4, 2004, Barcelona, Volume 2986 of Lecture Notes in Computer Science, pp. 3—17, © Springer.
  6. Antoine Miné.
    Weakly relational numerical abstract domains.
    Thèse de l'École polytechnique, 6 December 2004.

  7. Jérôme Feret.
    The arithmetic-geometric progression abstract domain.
    In VMCAI 2005 — Verification, Model Checking and Abstract Interpretation, R. Cousot (editor), Volume 3385 of Lecture Notes in Computer Science, pp. 42—58, 17—19 January 2005, Paris, © Springer.

  8. Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux & Xavier Rival.
    The Astrée analyser.
    In ESOP 2005 — The European Symposium on Programming, M. Sagiv (editor), Volume 3444 of Lecture Notes in Computer Science, pp. 21—30, 2—10 April 2005, Edinburgh, © Springer.
  9. Laurent Mauborgne & Xavier Rival.
    Trace Partitioning in Abstract Interpretation Based Static Analyzer.
    In ESOP 2005 — ; The European Symposium on Programming, M. Sagiv (editor), Volume 3444 of Lecture Notes in Computer Science, pp. 5—20, 2—10 April 2005, Edinburgh, © Springer.
  10. Xavier Rival.
    Understanding the Origin of Alarms in Astrée.
    In SAS'05 — The 12th International Static Analysis Symposium, Chris Hankin & Igor Siveroni (editors), Volume 3672 of Lecture Notes in Computer Science, pp. 303—319, 7—9 September 2005, London, UK, © Springer.
  11. David Monniaux.
    The Parallel Implementation of the Astree Static Analyzer.
    In APLAS 2005 — The Third Asian Symposium on Programming Languages and Systems, Kwangkeun Yi (editor), Volume 3780 of Lecture Notes in Computer Science, pp. 86—96, 2—5 November 2005, Tsukuba, Japan, © Springer.
  12. Xavier Rival.
    Abstract Dependences for Alarm Diagnosis.
    In APLAS 2005 — The Third Asian Symposium on Programming Languages and Systems, Kwangkeun Yi (editor), Volume 3780 of Lecture Notes in Computer Science, pp. 347—363, 2—5 November 2005, Tsukuba, Japan, © Springer.
  13. Antoine Miné.
    Symbolic Methods to Enhance the Precision of Numerical Abstract Domains.
    In VMCAI 2006 — Seventh International Conference on Verification, Model Checking and Abstract Interpretation, E. Allen Emerson & Kedar S. Namjoshi (editors), Volume 3855 of Lecture Notes in Computer Science, pp. 348—363, 8—10 January 2006, Charleston, South Carolina, USA, © Springer.
  14. Antoine Miné.
    Field-Sensitive Value Analysis of Embedded C Programs with Union Types and Pointer Arithmetics.
    In Proceedings of the 2006 ACM SIGPLAN/SIGBED Conference for Languages, Compilers, and Tools for Embedded Systems (LCTES 2006), 14—16 June 2006, Ottawa, Ontario, Canada. ACM Press, pp. 54—63.
  15. Patrick Cousot.
    L'analyseur statique Astrée  (french), Grand Colloque TIC 2006, Session RNTL « Systèmes embarqués », Centre de congrès, Lyon, 15 novembre 2006.
  16. Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, & Xavier Rival.
    Combination of Abstractions in the Astrée Static Analyzer. In 11th Annual Asian Computing Science Conference (ASIAN'06), National Center of Sciences, Tokyo, Japan, December 6—8, 2006. LNCS 4435, Springer, Berlin, pp. 272—300, 2008.
  17. Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival.
    Varieties of Static Analyzers: A Comparison with Astrée, invited paper.
    First IEEE & IFIP International Symposium on ``Theoretical Aspects of Software Engineering'', TASE'07, Shanghai, China, 6—8 June 2007, pp. 3—17.
  18. Patrick Cousot.
    Proving the Absence of Run-Time Errors in Safety-Critical Avionics Code.
    In EMSOFT 2007, Embedded Systems Week, Salzburg, Austria, September 30th, 2007, pp. 7—9, ACM Press.
  19. Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, and Xavier Rival.
    Why does Astrée scale up.
    Formal Methods in System Design, Springer, to appear, 2010.

Bibliographic References on the Industrial Use of Astrée

  1. David Delmas and Jean Souyris.
    Astrée: from Research to Industry.
    Proc. 14th International Static Analysis Symposium, SAS 2007, G. Filé & H. Riis-Nielson (eds), Kongens Lyngby, Denmark, 22-24 August 2007, LNCS 4634, pp. 437—451, © Springer, Berlin.
  2. Jean Souyris and David Delmas.
    Experimental Assessment of Astrée on Safety-Critical Avionics Software.
    Proc. Int. Conf. Computer Safety, Reliability, and Security, SAFECOMP 2007, Francesca Saglietti and Norbert Oster (Eds.), Nuremberg, Germany, September 18—21, 2007, Volume 4680 of Lecture Notes in Computer Science, pp. 479—490, © Springer, Berlin.
  3. O. Bouissou, E. Conquet, P. Cousot, R. Cousot, J. Feret, K. Ghorbal, E. Goubault, D. Lesens, L. Mauborgne, A. Miné, S. Putot, X. Rival, M. Turin.
    Space software validation using Abstract Interpretation.
    Proc. 13thData Systems in Aerospace, DASIA 2009, Istanbul, Turkey, 26-29 May 2009, © Eurospace, Paris.

News on Astrée in the press

Support of Astrée

RNTL      ANR       The development of the Astrée Analyzer was supported in part by the French exploratory project ASTRÉE of the Réseau National de recherche et d'innovation en Technologies Logicielles (RNTL, now Agence Nationale de la Recherche, ANR)  (french) (2002—2006). The final review of the ASTRÉE project was on July 7th, 2006.
 

Pictures of Astrée

ASTREE in NYC Poster Astrée ASTREE in ESOP'11
New York City, 6 Jan. 2007 Astrée poster, 9 Oct. 2007 fran\347ais Presentation by AbsInt at ESOP'2011
 

(‡) All spam emails to electronic contact to Astrée not containing ASTREE (in uppercase) in the subject are automatically filtered out.
Valid HTML 4.01 Transitional        Valid CSS!