The Astrée Static Analyzer

Centre National de la Recherche Scientifique

École Normale Supérieure

INRIA (since Sep. 2007)

Participants:

Former participants:

Contact(‡):

https://www.astree.ens.fr/

Astrée stands for Analyseur statique de logiciels temps-ré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).
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.
In April 2008, Astrée was able to prove completely automatically the absence of any RTE in a C version of the automatic docking software of the Jules Vernes Automated Transfer Vehicle (ATV) enabling ESA to transport payloads to the International Space Station [32].

Exploitation license of Astrée

Starting Dec. 2009, Astrée is available from AbsInt Angewandte Informatik   (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 »  ). 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:

• signal all possible errors (Astrée is always sound);
• occasionally signal errors that cannot really happen (false alarms on spurious executions e.g. when hypotheses on the execution environment are not taken into account).

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?

• Any use of C defined by the international norm governing the C programming language (ISO/IEC 9899:1999) as having an undefined behavior (such as division by zero or out of bounds array indexing),
• Any use of C violating the implementation-specific behavior of the aspects defined by ISO/IEC 9899:1999 as being specific to an implementation of the program on a given machine (such as the size of integers and arithmetic overflow),
• Any potentially harmful or incorrect use of C violating optional user-defined programming guidelines (such as no modular arithmetic for integers, even though this might be the hardware choice), and also
• Any violation of optional, user-provided assertions (similar to assert diagnostics for example), to prove user-defined run-time properties.

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;
    };
    /* ... */
  };
}

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
% 

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;
}

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 is sound, automatic, efficient, domain-aware, parametric, modular, extensible and precise

• Some static analyzers consider only some of the possible run-time errors while others sort out the most probable ones. The aim is then static testing (that is to find out the most frequent bugs) rather than verification (that is to prove the absence of any run-time error).
  In contrast Astrée is sound. Astrée will always exhaustively consider all possible run-time errors and never omit to signal a potential run-time error, a minimal requirement for safety critical software.
• Some static analyzers (e.g. using theorem provers) require programs to be decorated with inductive invariants.
  In contrast Astrée is fully automatic, that is never needs to rely on the user's help.
• Some static analyzers have high computational costs (typically hours of computation per 10,000 lines of code) while others may never terminate or terminate out of memory.
  In contrast Astrée has shown to be efficient and to scale up to real size programs as found in the industrial practice. Since 2005, Astrée can run on multicore parallel or distributed machines [21].
• General-purpose static analyzers aim at analyzing any program written in a given programming language and so can only rely on programming language-related properties to point at potential run-time errors.
• Specialized static analyzers put additional restriction on considered program and so can take specific program structures into account.
  In contrast, Astrée is domain-aware and so knows facts about application domains that are indispensable to make sophisticated proofs. For example, Astrée takes the logic and functional properties of control/command theory into account as implemented in control/command programs [12] [13].
  Moreover, Astrée is parametric. This means that the rate (cost of the analysis / precision of the analysis) can be fully adapted to the needs of Astrée's end-users thanks to parameters and directives tuning the abstraction.
  Astrée is modular. It is made of pieces (so called abstract domains) that can be assembled and parameterized to build application specific analyzers [27], fully adapted to a domain of application or to end-user needs. Written in OCaml, the modularization of Astrée is made easy thanks to OCaml's modules and functors.
  Finally, Astrée is extensible. In case of false alarms, it can be easily extended by introducing new abstract domains enhancing the precision of the analysis.
• A consequence of generality may be low precision. Typical rates of false alarms (i.e. spurious warnings on potential errors than can never occur at runtime) are from 10% to 20% of the C basic operations in the program.
• Specialized static analyzers achieve better precision (e.g. less than 10% of false alarms).
• Even a high selectivity rate of 1 false alarm over 100 operations with potential run-time errors leaves a number of doubtful cases which may be unacceptable for very large safety-critical or mission-critical software (for example, a selectivity rate of 1% yields 1000 false alarms on a program with 100 000 operations).
  In contrast Astrée, being modular, parametric and domain-aware can be made very precise and has shown to be able to produce no false alarm, that is fully automated correctness proofs.
  Theoretical work was done on locating the origin of alarms [20] [22].

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

Presentations of Astrée

• Presentation of the Astrée static analyzer on Tuesday August 24^th, 2004 at the topical day on abstract interpretation of the IFIP World Computer Congress in Toulouse (France).
• Presentation of Astrée on January 20^th, 2005 at the Industrial day on Automatic Tools for Program Verification, a satellite event of VMCAI'05, Paris, January 17—19, 2005.
• Presentation of Astrée on March 21^st, 2007 at the thirteenth ASTReNet Workshop on Formal Aspects of Source Code Analysis and Manipulation, BCS-FACS, London, England.
• Presentation of Astrée on December 8^th, 2007 at the 11^th Annual Asian Computing Science Conference, ASIAN'06, National Center of Sciences, Tokyo, Japan.
• Presentation of Astrée on June 5^th, 2007 at the First IEEE & IFIP International Symposium on Theoretical Aspects of Software Engineering, TASE 2007, Tutorial, Shanghai, China.
• Presentation of Astrée on October 11^th, 2007 at the Embedded Systems Week, Sept 30^th—Oct. 5^th, Salzburg, Austria.
• Présentation et démonstration d'Astrée  on October 11^th, 2007 at the XIV^es Rencontres INRIA - Industrie, INRIA Rocquencourt, France. 
• Presentation of Astrée on 16—17 October 2007 at the ES_PASS Workshop, Berlin, Germany.
• Presentation of Astrée on December 10^th 2007 at the School of Computer and Communication Sciences Seminar, École Polytechnique Fédérale de Lausanne (EPFL), Switzerland.
• Presentation of Astrée on December 12^th, 2007 at the 2007 ISoLA Workshop On Leveraging Applications of Formal Methods, Verification and Validation, Special Workshop Theme: Formal Methods in Avionics, Space and Transport, Poitiers, France.
• Présentation d'Astrée  on December 20^th, at the Séminaire du LINA, Laboratoire d'informatique de Nantes Atlantique, Nantes, France.
• Presentation of Astrée on January 18^th at the Seminar, Computer Science Department, Stony Brook University, Stony Brook, New York, USA.
• Presentation of Astrée on February 5^th, 2008 at the Seminar, Center for Computational and Systems Biology (COSBI), The Microsoft Research — University of Trento, Trento, Italy.
• Presentation of Astrée on February 19^th, 2008 at the Colloquia Patavina, Dipartimento di Matematica Pura ed Applicata, Università degli Studi di Padova, Padova, Italy.
• Presentation of Astrée on April 15^th, 2008 at the Dagstuhl seminar 08161, « Scalable Program Analysis », Schloss Dagstuhl, Germany.
• Presentation of Astrée on August 26^th, 2008 at the Max Planck Institute for Software Systems, Saarbrücken, Germany.
• Presentation of Astrée on September 19^th, 2008 at the Final review of the ESA ITI project Space Software Validation using Abstract Interpretation (SSVAI). Noordwijk, The Netherlands.
• Presentation of Astrée on October 30^th, 2008 at the Seoul National University, Computer Science & Engineering, Distinguished Lecture Series, Seoul, Korea.
• Presentation of Astrée on November 21^th, the Computer Science Colloquium, Computer Science, New York University, New York, NY, USA.
• Presentation of Astrée on December 4^th, 2008 at the Airbus workshop on formal verification tools strategy, Toulouse, France.
• Presentation of Astrée on January 18^th, 2009 at the Tenth International Conference on Verification, Model Checking, and Abstract Interpretation VMCAI'2009, Savannah, GA, USA.
• Presentation of Astrée on May 27^th, 2009 at the Doctorate Program PUMA, Program and Model Analysis (Graduiertenkolleg Programm- Und Modell-Analyse), Fakultät für Informatik, Technische Universität München and the Fakultät für Informatik, Ludwig-Maximilians-Universität München, Germany.

Astrée Flyer

• Astrée : Analyse statique de code C critique remps réel synchrone embarqué (pdf)  

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.

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

4. 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.
5. 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.
6. 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).
7. 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.
8. Patrick Cousot & Radhia Cousot.
   Abstract interpretation frameworks.
   Journal of Logic and Computation, 2(4):511—547, August 1992.
9. 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.
10. 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

11. 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.

12. 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.

13. 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.

14. 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.

15. 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.

16. Antoine Miné.
    Weakly relational numerical abstract domains.
    Thèse de l'École polytechnique, 6 December 2004.

17. 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.

18. 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.

19. 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.

20. 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.

21. 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.

22. 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.

23. 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.

24. 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.

25. Patrick Cousot.
    L'analyseur statique Astrée  , Grand Colloque TIC 2006, Session RNTL « Systèmes embarqués », Centre de congrès, Lyon, 15 novembre 2006.

26. 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 11^th 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.

27. 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.
28. Patrick Cousot.
    Proving the Absence of Run-Time Errors in Safety-Critical Avionics Code.
    In EMSOFT 2007, Embedded Systems Week, Salzburg, Austria, September 30^th, 2007, pp. 7—9, ACM Press.

29. 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

30. David Delmas and Jean Souyris.
    Astrée: from Research to Industry.
    Proc. 14^th 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.
31. 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.
32. 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. 13^thData Systems in Aerospace, DASIA 2009, Istanbul, Turkey, 26-29 May 2009, © Eurospace, Paris.

News on Astrée in the press

• Le Journal du CNRS, Nº 182, mars 2005, page 35, Le CNRS, l'A380 et l'aéronautique de demain.
• Le Monde, Nº 18741, 27 avril 2005, page 18, L'avion qui "bat des ailes" a fédéré de nombreux chercheurs.
• Software ohne Fehl und Tadel by Karlhorst Klotz, Das M.I.T. Magazin für Innovation Technology, 21 June 2005.
• Le Journal du CNRS, Nº 185, juin 2005, page 25, A380 : Le CNRS à la fête.
• Le Journal du CNRS, Nº 185, juin 2005, pages 25-27, Sécurité : toujours plus !
• Le Journal du CNRS, Nº 239, décembre 2009, page 14, Le CNRS décolle avec l'A380

Support of Astrée

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)   (2002—2006). The final review of the ASTRÉE project was on July 7th, 2006.

Pictures of Astrée

New York City, 6 Jan. 2007	Astrée poster, 9 Oct. 2007	Presentation by AbsInt at ESOP'2011

All spam emails to not containing ASTREE (in uppercase) in the subject are automatically filtered out.