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
Subtitle of host publicationSecure Software and Related Issues - 11th Asian Computing Science Conference, Revised Selected Papers
Pages272-300
Number of pages29
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)0302-9743
ISSN (Electronic)1611-3349

Other

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

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Combination of abstractions in the ASTRÉE static analyzer'. Together they form a unique fingerprint.

Cite this