Abstract
Automated methods for an undecidable class of verification problems cannot be complete (terminate for every correct program). We therefore consider a new kind of quality measure for such methods, which is completeness relative to a (powerful but unrealistic) oraclebased method. More precisely, we ask whether an often implemented method known as “software model checking with abstraction refinement” is complete relative to fixpoint iteration with “oracle-guided” widening. We show that whenever backward fixpoint iteration with oracle-guided widening succeeds in proving a property π (for some sequence of widenings determined by the oracle) then software model checking with a particular form of backward refinement will succeed in proving π. Intuitively, this means that the use of fixpoint iteration over abstractions and a particular backwards refinement of the abstractions has the effect of exploring the entire state space of all possible sequences of widenings.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
P. A. Abdulla, A. Annichini, S. Bensalem, A. Bouajjani, P. Habermehl, and Y. Lakhnech. Verification of infinite-state systems by combining abstraction and reachability analysis. In CAV 99: Computer-aided Verification, LNCS 1633, pages 146–159. Springer-Verlag, 1999.
T. Ball, R. Majumdar, T. Millstein, and S. K. Rajamani. Automatic predicate abstraction of C programs. In PLDI 01: Programming Language Design and Implementation, pages 203–213. ACM, 2001.
T. Ball, A. Podelski, and S. K. Rajamani. On the relative completeness of abstraction refinement. Technical Report MSR-TR-2001-106, Microsoft Research, 2001.
T. Ball and S. K. Rajamani. Automatically validating temporal safety properties of interfaces. In SPIN 01: SPIN Workshop, LNCS 2057, pages 103–122. Springer-Verlag, 2001.
R. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677–691, 1986.
E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In CAV 00: Computer Aided Verification, LNCS 1855, pages 154–169. Springer-Verlag, 2000.
E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In CAV 00: Computer-Aided Verification, LNCS 1855, pages 154–169. Springer-Verlag, 2000.
S. A. Cook. Soundness and completeness of an axiom system for program verification. SIAM Journal of Computing, 7(1):70–91, February 1978.
J. Corbett, M. Dwyer, J. Hatcliff, C. Pasareanu, Robby, S. Laubach, and H. Zheng. Bandera: Extracting finite-state models from Java source code. In ICSE 2000: International Conference on Software Engineering, pages 439–448. ACM, 2000.
P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In POPL 79: Principles of Programming Languages, pages 269–282. ACM, 1979.
P. Cousot and R. Cousot. Comparing the Galois connection and widening/narrowing approaches to abstract interpretation. In Proceedings of PLILP 92: Programming Language Implementation and Logic Programming, LNCS 631, pages 269–295. Springer-Verlag, 1992.
P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In POPL 78: Principles of Programming Languages, pages 84–96. ACM, 1978.
S. Das and D. L. Dill. Successive approximation of abstract transition relations. In LICS 01: Symposium on Logic in Computer Science, 2001.
S. Das, D. L. Dill, and S. Park. Experience with predicate abstraction. In CAV 00: Computer-Aided Verification, LNCS 1633, pages 160–171. Springer-Verlag, 1999.
G. Delzanno and A. Podelski. Model checking in CLP. In TACAS99: Tools and Algorithms for Construction and Analysis of Systems, LNCS 1579, pages 223–239. Springer-Verlag, 1999.
R. Giacobazzi and E. Quintarelli. Incompleteness, counterexamples and refinements in abstract model checking. In SAS 01: Static Analysis, LNCS 2126, pages 356–373. Springer-Verlag, 2001.
S. Graf and H. Saïdi. Construction of abstract state graphs with PVS. In CAV 97: Computer-aided Verification, LNCS 1254, pages 72–83. Springer-Verlag, 1997.
N. Halbwachs, Y.-E. Proy, and P. Raymond. Verification of linear hybrid systems by means of convex approximations. In SAS 94: Static Analysis, LNCS 864, pages 223–237. Springer-Verlag, 1994.
T. Henzinger and R. Majumdar. A classification of symbolic transition systems. In STACS 00: Theoretical Aspects of Computer Science, LNCS 1770, pages 13–34. Springer-Verlag, 2000.
T. A. Henzinger, P. Ho, and H. Wong-Toi. Hytech: a model checker for hybrid systems. Software Tools for Technology Transfer, 1:110–122, 1997.
T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. personal communication, May 2001.
B. Jeannet. Dynamic partitionning in linear relation analysis and application to the verification of synchronous programs. PhD thesis, Institut National Polytechnique de Grenoble, September 2000.
R. Kurshan. Computer-aided Verification of Coordinating Processes. Princeton University Press, 1994.
Y. Lakhnech. Personal communication, April 2001.
Y. Lakhnech, S. Bensalem, S. Berezin, and S. Owre. Incremental verification by abstraction. In TACAS01: Tools and Algorithms for Construction and Analysis of Systems, LNCS 2031, pages 98–112. Springer-Verlag, 2001.
K. S. Namjoshi and R. P. Kurshan. Syntactic program transformations for automatic abstraction. In CAV 00: Computer-Aided Verification, LNCS 1855, pages 435–449. Springer-Verlag, 2000.
V. Rusu and E. Singerman. On proving safety properties by integrating static analysis, theorem proving and abstraction. In TACAS99: Tools and Algorithms for Construction and Analysis of Systems, LNCS 1579, pages 178–192. Springer-Verlag, 1999.
M. Sagiv, T. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. In POPL 99: Principles of Programming Languages, pages 105–118. ACM, 1999.
H. Saïdi and N. Shankar. Abstract and model check while you prove. In CAV 99: Computer-aided Verification, LNCS 1633, pages 443–454. Springer-Verlag, 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ball, T., Podelski, A., Rajamani, S.K. (2002). Relative Completeness of Abstraction Refinement for Software Model Checking. In: Katoen, JP., Stevens, P. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2002. Lecture Notes in Computer Science, vol 2280. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46002-0_12
Download citation
DOI: https://doi.org/10.1007/3-540-46002-0_12
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43419-1
Online ISBN: 978-3-540-46002-2
eBook Packages: Springer Book Archive