• Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, & Xavier Rival.
  The ASTRÉE Analyzer.
  In Proceedings of Programming Languages and Systems, 14th European Symposium on Programming, ESOP 2005, Shmuel Sagiv (Ed.), Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, April 4—8, 2005, Edinburgh, UK. Lecture Notes in Computer Science 3444, pp. 21—30, © Springer, ISBN 3-540-25435-8.

  Paper: PDF (267.2 KB).

• Abstract:      ASTRÉE is an abstract interpretation-based static program analyzer aiming at proving automatically the absence of run time errors in programs written in the C programming language. It has been applied with success to large embedded control-command safety critical real-time software generated automatically from synchronous specifications, producing a correctness proof for complex software without any false alarm in a few hours of computation.

• Résumé:      ASTRÉE est un analyseur statique de programmes basé sur l'interprétation abstraite dont le but est de prouver automatiquement l'absence d'erreurs à l'exécution de programmes écrits dans le langage de programmation C. Il a été appliqué avec succès à de grands programmes embarqués critiques temps-réel, engendrés automatiquement à partir de spécifications synchrones, produisant une preuve de correction de logiciels complexes en quelques heures de calcul.

• Slides of the 30mn presentation: .pdf (95.4 KB).

-->

\bibitem{CousotEtAl-ASTREE-ESOP05}
P{.}~Cousot, R{.}~Cousot, J{.}~Feret, L{.}~Mauborgne, A{.}~Min\'e, D{.}~Monniaux, and X{.}~Rival.  
\newblock The {ASTR\'EE} {A}nalyser.
\newblock \emph{Proc{.} European Symp{.} on Programming} (ESOP'05), Edinburgh, Scotland, April
2--10, 2005, LNCS 3444, M{.}~Sagiv (Ed.), pp{.} 21--30.  \textcopyright\ Springer, 2005.

@InProceedings{CousotEtAl-ASTREE-ESOP05,
   author =    {P{.}~Cousot and  R{.}~Cousot and J{.}~Feret and L{.}~Mauborgne 
                and A{.}~Min\'e and D{.}~Monniaux and X{.}~Rival},
   title =     {The {ASTR\'EE} {A}nalyser},
   pages =     {21--30},
   booktitle = {Proceedings of the European Symposium on Programming (ESOP'05)},
   series =    {Lecture Notes in Computer Science},
   editor =    {M{.}~Sagiv},
   volume =    {3444},
   address =   {Edinburgh, Scotland},
   publisher = {\textcopyright\ Springer},
   month =     {April 2--10},
   year =      2005,
}