Combination of abstractions in the ASTRÉE static analyzer

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

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

Abstract

We describe the structure of the abstract domains in the Astrée static analyzer, their modular organization into a hierarchical network, their cooperation to over-approximate the conjunction/reduced product of different abstractions and to ensure termination using collaborative widenings and narrowings. This separation of the abstraction into a combination of cooperative abstract domains makes Astrée extensible, an essential feature to cope with false alarms and ultimately provide sound formal verification of the absence of runtime errors in very large software.

Original languageEnglish (US)
Title of host publicationAdvances in Computer Science - ASIAN 2006: Secure Software and Related Issues - 11th Asian Computing Science Conference, Revised Selected Papers
Pages272-300
Number of pages29
Volume4435 LNCS
DOIs
StatePublished - 2007
Event11th Asian Computing Science Conference, ASIAN 2006 - Tokyo, Japan
Duration: Dec 6 2006Dec 8 2006

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4435 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other11th Asian Computing Science Conference, ASIAN 2006
CountryJapan
CityTokyo
Period12/6/0612/8/06

Fingerprint

Software
Acoustic waves
Hierarchical Networks
Formal Verification
False Alarm
Termination
Abstraction
Formal verification
Sound

ASJC Scopus subject areas

  • Computer Science(all)
  • Biochemistry, Genetics and Molecular Biology(all)
  • Theoretical Computer Science

Cite this

Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., & Rival, X. (2007). Combination of abstractions in the ASTRÉE static analyzer. In Advances in Computer Science - ASIAN 2006: Secure Software and Related Issues - 11th Asian Computing Science Conference, Revised Selected Papers (Vol. 4435 LNCS, pp. 272-300). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4435 LNCS). https://doi.org/10.1007/978-3-540-77505-8_23

Combination of abstractions in the ASTRÉE static analyzer. / Cousot, Patrick; Cousot, Radhia; Feret, Jérôme; Mauborgne, Laurent; Miné, Antoine; Monniaux, David; Rival, Xavier.

Advances in Computer Science - ASIAN 2006: Secure Software and Related Issues - 11th Asian Computing Science Conference, Revised Selected Papers. Vol. 4435 LNCS 2007. p. 272-300 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4435 LNCS).

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

Cousot, P, Cousot, R, Feret, J, Mauborgne, L, Miné, A, Monniaux, D & Rival, X 2007, Combination of abstractions in the ASTRÉE static analyzer. in Advances in Computer Science - ASIAN 2006: Secure Software and Related Issues - 11th Asian Computing Science Conference, Revised Selected Papers. vol. 4435 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 4435 LNCS, pp. 272-300, 11th Asian Computing Science Conference, ASIAN 2006, Tokyo, Japan, 12/6/06. https://doi.org/10.1007/978-3-540-77505-8_23
Cousot P, Cousot R, Feret J, Mauborgne L, Miné A, Monniaux D et al. Combination of abstractions in the ASTRÉE static analyzer. In Advances in Computer Science - ASIAN 2006: Secure Software and Related Issues - 11th Asian Computing Science Conference, Revised Selected Papers. Vol. 4435 LNCS. 2007. p. 272-300. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-540-77505-8_23
Cousot, Patrick ; Cousot, Radhia ; Feret, Jérôme ; Mauborgne, Laurent ; Miné, Antoine ; Monniaux, David ; Rival, Xavier. / Combination of abstractions in the ASTRÉE static analyzer. Advances in Computer Science - ASIAN 2006: Secure Software and Related Issues - 11th Asian Computing Science Conference, Revised Selected Papers. Vol. 4435 LNCS 2007. pp. 272-300 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{9f0b28ec39054807a601f52a5bafdbec,
title = "Combination of abstractions in the ASTR{\'E}E static analyzer",
abstract = "We describe the structure of the abstract domains in the Astr{\'e}e static analyzer, their modular organization into a hierarchical network, their cooperation to over-approximate the conjunction/reduced product of different abstractions and to ensure termination using collaborative widenings and narrowings. This separation of the abstraction into a combination of cooperative abstract domains makes Astr{\'e}e extensible, an essential feature to cope with false alarms and ultimately provide sound formal verification of the absence of runtime errors in very large software.",
author = "Patrick Cousot and Radhia Cousot and J{\'e}r{\^o}me Feret and Laurent Mauborgne and Antoine Min{\'e} and David Monniaux and Xavier Rival",
year = "2007",
doi = "10.1007/978-3-540-77505-8_23",
language = "English (US)",
isbn = "3540775048",
volume = "4435 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "272--300",
booktitle = "Advances in Computer Science - ASIAN 2006: Secure Software and Related Issues - 11th Asian Computing Science Conference, Revised Selected Papers",

}

TY - GEN

T1 - Combination of abstractions in the ASTRÉE static analyzer

AU - Cousot, Patrick

AU - Cousot, Radhia

AU - Feret, Jérôme

AU - Mauborgne, Laurent

AU - Miné, Antoine

AU - Monniaux, David

AU - Rival, Xavier

PY - 2007

Y1 - 2007

N2 - We describe the structure of the abstract domains in the Astrée static analyzer, their modular organization into a hierarchical network, their cooperation to over-approximate the conjunction/reduced product of different abstractions and to ensure termination using collaborative widenings and narrowings. This separation of the abstraction into a combination of cooperative abstract domains makes Astrée extensible, an essential feature to cope with false alarms and ultimately provide sound formal verification of the absence of runtime errors in very large software.

AB - We describe the structure of the abstract domains in the Astrée static analyzer, their modular organization into a hierarchical network, their cooperation to over-approximate the conjunction/reduced product of different abstractions and to ensure termination using collaborative widenings and narrowings. This separation of the abstraction into a combination of cooperative abstract domains makes Astrée extensible, an essential feature to cope with false alarms and ultimately provide sound formal verification of the absence of runtime errors in very large software.

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

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

U2 - 10.1007/978-3-540-77505-8_23

DO - 10.1007/978-3-540-77505-8_23

M3 - Conference contribution

AN - SCOPUS:49949103829

SN - 3540775048

SN - 9783540775041

VL - 4435 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 272

EP - 300

BT - Advances in Computer Science - ASIAN 2006: Secure Software and Related Issues - 11th Asian Computing Science Conference, Revised Selected Papers

ER -