The ASTRÉE analyzer

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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)
Title of host publicationLecture Notes in Computer Science
EditorsM. Sagiv
Pages21-30
Number of pages10
Volume3444
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

Other

Other14th European Symposium on Programming, ESOP 2005, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005
CountryUnited Kingdom
CityEdinburgh
Period4/4/054/8/05

Fingerprint

Computer programming languages
Specifications

ASJC Scopus subject areas

  • Computer Science (miscellaneous)

Cite this

Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., & Rival, X. (2005). The ASTRÉE analyzer. In M. Sagiv (Ed.), Lecture Notes in Computer Science (Vol. 3444, pp. 21-30)

The ASTRÉE analyzer. / Cousot, Patrick; Cousot, Radhia; Feret, Jerôme; Mauborgne, Laurent; Miné, Antoine; Monniaux, David; Rival, Xavier.

Lecture Notes in Computer Science. ed. / M. Sagiv. Vol. 3444 2005. p. 21-30.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Cousot, P, Cousot, R, Feret, J, Mauborgne, L, Miné, A, Monniaux, D & Rival, X 2005, The ASTRÉE analyzer. in M Sagiv (ed.), Lecture Notes in Computer Science. vol. 3444, pp. 21-30, 14th 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, 4/4/05.
Cousot P, Cousot R, Feret J, Mauborgne L, Miné A, Monniaux D et al. The ASTRÉE analyzer. In Sagiv M, editor, Lecture Notes in Computer Science. Vol. 3444. 2005. p. 21-30
Cousot, Patrick ; Cousot, Radhia ; Feret, Jerôme ; Mauborgne, Laurent ; Miné, Antoine ; Monniaux, David ; Rival, Xavier. / The ASTRÉE analyzer. Lecture Notes in Computer Science. editor / M. Sagiv. Vol. 3444 2005. pp. 21-30
@inproceedings{98e19ed52e984f7e8c48c14a16a2bfa2,
title = "The ASTR{\'E}E analyzer",
abstract = "ASTR{\'E}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.",
author = "Patrick Cousot and Radhia Cousot and Jer{\^o}me Feret and Laurent Mauborgne and Antoine Min{\'e} and David Monniaux and Xavier Rival",
year = "2005",
language = "English (US)",
volume = "3444",
pages = "21--30",
editor = "M. Sagiv",
booktitle = "Lecture Notes in Computer Science",

}

TY - GEN

T1 - The ASTRÉE analyzer

AU - Cousot, Patrick

AU - Cousot, Radhia

AU - Feret, Jerôme

AU - Mauborgne, Laurent

AU - Miné, Antoine

AU - Monniaux, David

AU - Rival, Xavier

PY - 2005

Y1 - 2005

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

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

UR - http://www.scopus.com/inward/record.url?scp=24644450827&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=24644450827&partnerID=8YFLogxK

M3 - Conference contribution

AN - SCOPUS:24644450827

VL - 3444

SP - 21

EP - 30

BT - Lecture Notes in Computer Science

A2 - Sagiv, M.

ER -