Abstract
We show how to attack the problem of model checking a C program with recursive procedures using an abstraction that we formally define as the composition of the Boolean and the Cartesian abstractions. It is implemented through a source-to-source transformation into a ‘Boolean’ C program; we give an algorithm to compute the transformation with a cost that is exponential in its theoretical worst-case complexity but feasible in practice.
On leave from Max Planck Institute, Saarbrücken, Germany.
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
T. Ball, R. Majumdar, T. Millstein, and S. K. Rajamani. Automatic predicate abstraction of C programs. In Proceedings of SIGPLAN Conference on Proramming Language Design and Implementation, 2001 (to appear). ACM, 2001.
T. Ball and S. K. Rajamani. Bebop: A symbolic model checker for Boolean programs. In SPIN 00: SPIN Workshop, LNCS 1885, pages 113–130. Springer-Verlag, 2000.
E. M. Clarke and E. A. Emerson. Synthesis of synchronization skeletons for branching time temporal logic. In Logic of Programs, LNCS 131, pages 52–71. Springer-Verlag, 1981.
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.
E. M. Clarke, O. Grumberg, and D. Long. Model checking and abstraction. In POPL 92: Principles of Programming Languages, pages 343–354. ACM, 1992.
R. Cleaveland, P. Iyer, and D. Yankelevich. Optimality in abstractions of model checking. In SAS 95: Static Analysis, LNCS 983, pages 51–63. Springer-Verlag, 1995.
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. Abstract interpretation: a unified lattice model for the static analysis of programs by construction or approximation of fixpoints. In POPL 77: Principles of Programming Languages, pages 238–252. ACM, 1977.
P. Cousot and R. Cousot. Formal language, grammar and set-constraint-based program analysis by abstract interpretation. In FPCA 95: Functional Programming and Computer Architecture, pages 170–181. ACM, 1995.
D. Dams, O. Grumberg, and R. Gerth. Abstract interpretation of reactive systems: abstractions preserving ACTL?, ECTL?, and CTL?. In PROCOMET 94: Programming Concepts, Methods, and Calculi, pages 561–581. Elsevier Science Publishers, 1994.
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.
R. Giacobazzi, F. Ranzato, and F. Scozzari. Making abstract interpretations complete. Journal of the ACM, 47(2):361–416, March 2000.
S. Graf and H. Saidi. Construction of abstract state graphs with PVS. In CAV 97: Computer Aided Verification, LNCS 1254, pages 72–83. Springer-Verlag, 1997.
M. Huth, R. Jagadeesan, and D. A. Schmidt. Modal transition systems: a foundation for three-valued program analysis. In ESOP 01: European Symposium on Programming. Springer-Verlag, 2001. To appear.
R. Kurshan. Computer-aided Verification of Coordinating Processes. Princeton University Press, 1994.
C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, and S. Bensalem. Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design Volume, 6(1):11–44, 1995.
A. Podelski. Model checking as constraint solving. In SAS 00: Static Analysis, LNCS 1824, pages 221–37. Springer-Verlag, 2000.
T. Reps. Program analysis via graph reachability. Information and Software Technology, 40(11–12):701–726, November-December 1998.
T. Reps, S. Horwitz, and M. Sagiv. Precise interprocedural dataflow analysis via graph reachability. In POPL 95: Principles of Programming Languages, pages 49–61. ACM, 1995.
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.
D. Schmidt. Data flow analysis is model checking of abstract interpretation. In POPL 98: Principles of Programming Languages, pages 38–48. ACM, 1998.
M. Sharir and A. Pnueli. Two approaches to interprocedural data dalow analysis. In Program Flow Analysis: Theory and Applications, pages 189–233. Prentice-Hall, 1981.
B. Steffen. Data flow analysis as model checking. In TACS 91: Theoretical Aspects of Computer Science, LNCS 536, pages 346–365. Springer-Verlag, 1991.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ball, T., Podelski, A., Rajamani, S.K. (2001). Boolean and Cartesian Abstraction for Model Checking C Programs. In: Margaria, T., Yi, W. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2001. Lecture Notes in Computer Science, vol 2031. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45319-9_19
Download citation
DOI: https://doi.org/10.1007/3-540-45319-9_19
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41865-8
Online ISBN: 978-3-540-45319-2
eBook Packages: Springer Book Archive