Fixpoint-guided abstraction refinements

Patrick Cousot; Pierre Ganty; Jean François Raskin

doi:10.1007/978-3-540-74061-2_21

Fixpoint-guided abstraction refinements

Patrick Cousot, Pierre Ganty, Jean François Raskin

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English (US)
Title of host publication	Static Analysis - 14th International Symposium, SAS 2007, Proceedings
Publisher	Springer Verlag
Pages	333-348
Number of pages	16
ISBN (Print)	9783540740605
DOIs	https://doi.org/10.1007/978-3-540-74061-2_21
State	Published - 2007
Event	14th International Static Analysis Symposium, SAS 2007 - Kongens Lyngby, Denmark Duration: Aug 22 2007 → Aug 24 2007

Publication series

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

Other

Other	14th International Static Analysis Symposium, SAS 2007
Country/Territory	Denmark
City	Kongens Lyngby
Period	8/22/07 → 8/24/07

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-540-74061-2_21

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

Fixpoint-guided abstraction refinements. / Cousot, Patrick; Ganty, Pierre; Raskin, Jean François.
Static Analysis - 14th International Symposium, SAS 2007, Proceedings. Springer Verlag, 2007. p. 333-348 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4634 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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

@inproceedings{bb81c1421b3d44a4978e9876bb14d079,

title = "Fixpoint-guided abstraction refinements",

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

author = "Patrick Cousot and Pierre Ganty and Raskin, {Jean Fran{\c c}ois}",

year = "2007",

doi = "10.1007/978-3-540-74061-2_21",

language = "English (US)",

isbn = "9783540740605",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "333--348",

booktitle = "Static Analysis - 14th International Symposium, SAS 2007, Proceedings",

note = "14th International Static Analysis Symposium, SAS 2007 ; Conference date: 22-08-2007 Through 24-08-2007",

}

TY - GEN

T1 - Fixpoint-guided abstraction refinements

AU - Cousot, Patrick

AU - Ganty, Pierre

AU - Raskin, Jean François

PY - 2007

Y1 - 2007

N2 - 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.

AB - 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.

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

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

U2 - 10.1007/978-3-540-74061-2_21

DO - 10.1007/978-3-540-74061-2_21

M3 - Conference contribution

AN - SCOPUS:38149039417

SN - 9783540740605

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

SP - 333

EP - 348

BT - Static Analysis - 14th International Symposium, SAS 2007, Proceedings

PB - Springer Verlag

T2 - 14th International Static Analysis Symposium, SAS 2007

Y2 - 22 August 2007 through 24 August 2007

ER -

Fixpoint-guided abstraction refinements

Abstract

Publication series

Other

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this