Name
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. |
Year | DOI | Venue |
|---|---|---|
2007 | 10.1007/978-3-540-74061-2_21 | static analysis symposium |
Keywords | DocType | Volume |
automatic refinement technique,abstract domain,automatic refinement,nested loop,so-called acceleration technique,state space,abstract fixpoint checking algorithm,fixpoint-guided abstraction refinement,abstract refinement algorithm | Conference | 4634 |
ISSN | ISBN | Citations |
0302-9743 | 3-540-74060-0 | 26 |
PageRank | References | Authors |
0.92 | 16 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Patrick Cousot | 1 | 7721 | 574.52 |
| Pierre Ganty | 2 | 242 | 20.29 |
| Jean-François Raskin | 3 | 1735 | 100.15 |