The ASTRÉE analyzer

Patrick Cousot, Radhia Cousot, Jerôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, Xavier Rival

Research output: Contribution to journalConference article

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.

Original languageEnglish (US)
Pages (from-to)21-30
Number of pages10
JournalLecture Notes in Computer Science
Volume3444
DOIs
StatePublished - 2005
Event14th European Symposium on Programming, ESOP 2005, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005 - Edinburgh, United Kingdom
Duration: Apr 4 2005Apr 8 2005

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'The ASTRÉE analyzer'. Together they form a unique fingerprint.

  • Cite this

    Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., & Rival, X. (2005). The ASTRÉE analyzer. Lecture Notes in Computer Science, 3444, 21-30. https://doi.org/10.1007/978-3-540-31987-0_3