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

doi:10.1007/978-3-540-77505-8_23

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

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English (US)
Title of host publication	Advances in Computer Science - ASIAN 2006
Subtitle of host publication	Secure Software and Related Issues - 11th Asian Computing Science Conference, Revised Selected Papers
Pages	272-300
Number of pages	29
DOIs	https://doi.org/10.1007/978-3-540-77505-8_23
State	Published - 2007
Event	11th Asian Computing Science Conference, ASIAN 2006 - Tokyo, Japan Duration: Dec 6 2006 → Dec 8 2006

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	4435 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Other

Other	11th Asian Computing Science Conference, ASIAN 2006
Country/Territory	Japan
City	Tokyo
Period	12/6/06 → 12/8/06

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

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

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 (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 et al.
Advances in Computer Science - ASIAN 2006: Secure Software and Related Issues - 11th Asian Computing Science Conference, Revised Selected Papers. 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 proceeding › Conference 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. 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. 2007. p. 272-300. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-540-77505-8_23

Cousot, Patrick ; Cousot, Radhia ; Feret, Jérôme et al. / 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. 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",

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",

}

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

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

T2 - 11th Asian Computing Science Conference, ASIAN 2006

Y2 - 6 December 2006 through 8 December 2006

ER -

Combination of abstractions in the ASTRÉE static analyzer

Abstract

Publication series

Other

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this