The Astrée Static Analyzer
Participants:
Former participants:
Astrée stands for
Analyseur
statique de logiciels tempsréel
embarqués (realtime 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, timetriggered, realtime,
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
flybywire system, a program of 132,000 lines of C analyzed in
1^{h}20 on a 2.8 GHz 32bit PC using 300 Mb of memory
(and 50mn on a 64bit 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.



  



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 runtime 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 runtime 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 interpretationbased
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 costeffective, e.g. being a small fraction of the costs of running all tests of the program. In the context of
safetycritical 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 contextsensitive 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 generalpurpose abstractions are either nonrelationals (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 domainspecific 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
concretizationbased [8] in absence of best abstraction.
Which Program RunTime 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 RunTime Errors (RTE)
during any execution in any environment. This covers:
 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 implementationspecific 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
userdefined programming guidelines (such as no modular arithmetic
for integers, even though this might be the hardware choice),
and also
 Any violation of optional, userprovided assertions (similar to
assert
diagnostics for example), to prove
userdefined runtime properties.
Astrée is parameterized so as to be
adaptable to the enduser 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 runtime 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
runtime error (integer dividebyzero can never happen when executing
this program).
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:
/* floaterror.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 floaterror.c
% ./a.out
0.000000
% 
/* doubleerror.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 doubleerror.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)(xa) = 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 runtime 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 = x1.0e21;
x = yz;
}}
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, domainaware, parametric, modular, extensible and precise

Some static analyzers consider only some of the possible runtime 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 runtime error).
In contrast Astrée is sound.
Astrée will always exhaustively consider
all possible runtime errors and never omit to signal a potential
runtime 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].

Generalpurpose static analyzers
aim at analyzing any program written in a given programming language and so can
only rely on programming languagerelated properties to point at potential
runtime errors.
 Specialized static analyzers put
additional restriction on considered program and so can take specific
program structures into account.
In contrast,
Astrée is
domainaware 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 endusers 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 enduser 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 runtime errors leaves a number of doubtful
cases which may be unacceptable for very large safetycritical or
missioncritical 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 domainaware 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, BCSFACS, 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 ModellAnalyse), Fakultät für Informatik, Technische Universität München and the Fakultät für Informatik, LudwigMaximiliansUniversität München, Germany.
Astrée Flyer
Introductory Bibliographic References on Abstract Interpretation
 Patrick Cousot.
Interprétation abstraite.
Technique et Science Informatique, Vol. 19, Nb 123.
Janvier 2000, Hermès, Paris, France. pp. 155—164.
 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.
 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

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.

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 SIGPLANSIGACT Symposium on
Principles of Programming Languages, pages 238—252, Los Angeles,
California, 1977. ACM Press, New York.

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, StAndrews, N.B., Canada, 1977.
NorthHolland Publishing Company (1978).

Patrick Cousot & Radhia Cousot.
Systematic Design of Program Analysis Frameworks.
In
Conference Record of the Sixth Annual ACM SIGPLANSIGACT Symposium on
Principles of Programming Languages, pages 269—282, San Antonio,
Texas, 1979. ACM Press, New York.

Patrick Cousot & Radhia Cousot.
Abstract interpretation frameworks.
Journal of Logic and Computation,
2(4):511—547, August 1992.

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. © SpringerVerlag, Berlin, Germany, 1992.

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

Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux & Xavier Rival.
Design and Implementation of a SpecialPurpose Static Program Analyzer for SafetyCritical RealTime 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.

Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, & Xavier Rival.
A Static Analyzer for Large SafetyCritical 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.

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.

Laurent Mauborgne.
Astrée: verification of absence of runtime error.
In Building the Information Society, R. Jacquard
(Ed.), Kluwer Academic Publishers,
pp. 385—392, 2004.

Antoine Miné.
Relational abstract domains for the detection of floatingpoint
runtime 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.

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

Jérôme Feret.
The arithmeticgeometric 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.

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.

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.

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.

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.

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.

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.

Antoine Miné.
FieldSensitive 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.

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.

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.

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.

Patrick Cousot.
Proving the Absence of RunTime Errors in SafetyCritical Avionics Code.
In
EMSOFT 2007,
Embedded Systems Week,
Salzburg, Austria, September 30^{th}, 2007, pp. 7—9, ACM Press.

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
 David Delmas and Jean Souyris.
Astrée: from Research to Industry.
Proc. 14^{th} International Static Analysis Symposium, SAS 2007, G. Filé & H. RiisNielson (eds), Kongens Lyngby, Denmark, 2224 August 2007, LNCS 4634, pp. 437—451, © Springer, Berlin.
 Jean Souyris and David Delmas.
Experimental Assessment of Astrée on SafetyCritical 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.
 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^{th}Data Systems in Aerospace, DASIA 2009, Istanbul, Turkey, 2629 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 2527, 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 7^{th}, 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.