P. Cousot, P. Ganty, & J.F. Raskin, Fixpoint-Guided Abstraction Refinements

Patrick Cousot, Pierre Ganty, Jean-François Raskin.
Fixpoint-Guided Abstraction Refinements.
In 14^th Fourteenth International Symposium on Static Analysis, (SAS'07), The Technical University of Denmark, Kongens Lyngby, Denmark, August 22—24, 2006. LNCS 4634, © Springer-Verlag, Berlin, pp. 333—348.
Paper:
- Compressed PostScript .ps.gz (3 Mb),
- PDF (288 Kb)
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.
Keywords:
Abstract Interpretation, Abstraction, Acceleration techniques, Boolean closed domains, Completion, Fixpoint, CEGAR, Moore closed domains, Moore family, Refinement.

Bibliographic reference:

\bibitem{CousotGantyRaskin07-SAS}
P. Cousot, P. Ganty, & J.-F. Raskin.
\newblock Fixpoint-Guided Abstraction Refinements.
\newblock In \emph{Proc. Fourteenth International Symposium  
on Static Analysis (SAS$\,$'{07})}, G.\ Fil\'e \& H.\  Riis-Nielson (Eds), pages 
          333--348, Kongens Lyngby, Denmark, 22--24 August 2007.  Lecture Notes in Computer
	  Science, volume 4634, Springer, Berlin, pp. 333--348.

@inCollection{CousotGantyRaskin07-SAS,
   author =    {Cousot, P{.} and Ganty, P{.} and Raskin, J{.}-F{.}},
   title =     {Fixpoint-Guided Abstraction Refinements},
   booktitle = {Proceedings of the Fourteenth International Symposium  on Static Analysis, SAS$\,$'{07}},
   editor =    {Fil\'e, G{.} and Riis Nielson, H{.}},
   month =     {22--24 August},
   year =      2007,
   series =    {Kongens Lyngby, Denmark, Lecture Notes in Computer Science 4634},
   pages =     {333--348},
   publisher = {Springer, Berlin, Germany},
}

copyright notice, Springer copyright
Last modified: Monday, 04-Jan-2010 13:26:27 CET