Fixpoint-guided abstraction refinements

Patrick Cousot, Pierre Ganty, Jean François Raskin

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

Abstract

In this paper, we present an abstract fixpoint checking algorithm with automatic refinement by backward completion in Moore closed abstract domains. We study the properties of our algorithm and prove it to be more precise than the counterexample guided abstract refinement algorithm (CEGAR). Contrary to several works in the literature, our algorithm does not require the abstract domains to be partitions of the state space. We also show that our automatic refinement technique is compatible with so-called acceleration techniques. Furthermore, the use of Boolean closed domains does not improve the precision of our algorithm. The algorithm is illustrated by proving properties of programs with nested loops.

Original languageEnglish (US)
Title of host publicationStatic Analysis - 14th International Symposium, SAS 2007, Proceedings
PublisherSpringer Verlag
Pages333-348
Number of pages16
ISBN (Print)9783540740605
DOIs
StatePublished - 2007
Event14th International Static Analysis Symposium, SAS 2007 - Kongens Lyngby, Denmark
Duration: Aug 22 2007Aug 24 2007

Publication series

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

Other

Other14th International Static Analysis Symposium, SAS 2007
CountryDenmark
CityKongens Lyngby
Period8/22/078/24/07

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Fixpoint-guided abstraction refinements'. Together they form a unique fingerprint.

  • Cite this

    Cousot, P., Ganty, P., & Raskin, J. F. (2007). Fixpoint-guided abstraction refinements. In Static Analysis - 14th International Symposium, SAS 2007, Proceedings (pp. 333-348). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4634 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-540-74061-2_21