Fixpoint-guided abstraction refinements

Patrick Cousot, Pierre Ganty, Jean François Raskin

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


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
Number of pages16
ISBN (Print)9783540740605
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


Other14th International Static Analysis Symposium, SAS 2007
CityKongens Lyngby

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


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

Cite this