Abstract
Symbolic software verification engines such as Slam and ESC/Java often use automatic theorem provers to implement forms of symbolic simulation. The theorem provers that are used, such as Simplify, usually combine decision procedures for the theories of uninterpreted functions, linear arithmetic, and sometimes bit vectors using techniques proposed by Nelson-Oppen or Shostak. Programming language constructs such as pointers, structures and unions are not directly supported by the provers, and are often encoded imprecisely using axioms and uninterpreted functions.
In this paper we describe a more direct and accurate approach towards providing symbolic infrastructure for program verification engines. We propose the use of a theorem prover called Cogent, which provides better accuracy for ANSI-C expressions with the possibility of nested logic quantifiers. The prover’s implementation is based on a machine-level interpretation of expressions into propositional logic. Cogent’s translation allows the program verification tools to better reason about finite machine-level variables, bit operations, structures, unions, references, pointers and pointer arithmetic.
This paper also provides experimental evidence that the proposed approach is practical when applied to industrial program verification.
This paper is an extended version of [1].
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Cook, B., Sharygina, N., Kröning, D.: Cogent: Accurate Theorem Proving for Program Verification. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 296–300. Springer, Heidelberg (2005)
Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: PLDI 2002: Programming Language Design and Implementation (2002)
Barnett, M., DeLine, R., Fahndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. Journal of Object Technology 3, 27–56 (2004)
Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: A theorem prover for program checking.Technical Report HPL-2003-148, HP Labs (2003)
Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: PLDI 2001: Programming Language Design and Implementation, pp. 203–213. ACM, New York (2001)
Ball, T., Rajamani, S.K.: Generating abstract explanations of spurious counterexamples in C programs. Technical Report MSR-TR-2002-09, Microsoft Research (2002)
Ball, T., Cook, B., Das, S., Rajamani, S.K.: Refining Approximations in Software Predicate Abstraction. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 388–403. Springer, Heidelberg (2004)
Ball, T., Rajamani, S.K.: Bebop: A symbolic model checker for Boolean programs. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 113–130. Springer, Heidelberg (2000)
Ball, T., Rajamani, S.K.: Automatically validating temporal safety properties of interfaces. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 113–130. Springer, Heidelberg (2000)
Ball, T., Rajamani, S.K.: Bebop: A path-sensitive interprocedural dataflow engine. In: PASTE 2001: Workshop on Program Analysis for Software Tools and Engineering, pp. 97–103. ACM, New York (2001)
Ball, T., Cook, B., Lahiri, S.K., Zhang, L.: Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 457–461. Springer, Heidelberg (2004)
Henzinger, T.A., Jhala, R., Majumdar, R., Qadeer, S.: Thread-Modular Abstraction Refinement. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 262–274. Springer, Heidelberg (2003)
Chaki, S., Clarke, E., Groce, A., Strichman, O.: Predicate abstraction with minimum predicates. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 19–34. Springer, Heidelberg (2003)
Lakhnech, Y., Bensalem, S., Berezin, S., Owre, S.: Incremental verification by abstraction. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, p. 98. Springer, Heidelberg (2001)
Owre, S., Shankar, N., Rushby, J.: PVS: A prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607. Springer, Heidelberg (1992)
Barrett, C., Berezin, S.: CVC Lite: A New Implementation of the Cooperating Validity Checker Category B. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 515–518. Springer, Heidelberg (2004)
Filliatre, J.C., Owre, S., Rue, H., Shankar, N.: ICS: Integrated Canonizer and Solver. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 246. Springer, Heidelberg (2001)
Flanagan, C., Joshi, R., Ou, X., Saxe, J.B.: Theorem Proving Using Lazy Proof Explication. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 355–367. Springer, Heidelberg (2003)
Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems 1, 245–257 (1979)
Shostak, R.E.: Deciding combinations of theories. Journal of the ACM 31, 1–12 (1984)
Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004)
Bryant, R.E., Lahiri, S.K., Seshia, S.A.: Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 78. Springer, Heidelberg (2002)
International Organization for Standardization: ISO/IEC 9899:1999: Programming languages — C. International Organization for Standardization, Geneva, Switzerland (1999)
Kurshan, R.: Computer-Aided Verification of Coordinating Processes. Princeton University Press, Princeton (1995)
Ball, T., Cook, B., Levin, V., Rajamani, S.K.: SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol. 2999, pp. 1–20. Springer, Heidelberg (2004)
Lahiri, S.K., Bryant, R.E., Cook, B.: A Symbolic Approach to Predicate Abstraction. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 141–153. Springer, Heidelberg (2003)
Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: Predicate abstraction of ANSI–C programs using SAT. Technical Report CMU-CS-03-186, Carnegie Mellon University, School of Computer Science (2003)
Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: Predicate abstraction of ANSI–C programs using SAT. Formal Methods in System Design 25, 105–127 (2004)
Aagaard, M., Jones, R., Melham, T., O’Leary, J., Seger, C.J.H.: A methodology for large scale hardware verification. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517. Springer, Heidelberg (2002)
Grundy, J.: Verified optimizations for the Intel IA-64 architecture. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol. 1869. Springer, Heidelberg (2000)
Barret, C.W., Dill, D.L., Levitt, J.R.: A decision procedure for bit-vector arithmetic. In: DAC 1998: Design Automation Conference (1998)
Bush, W.R., Pincus, J.D., Sielaff, D.J.: A static analyzer for finding dynamic programming errors. Software—Practice and Experience 30, 775–802 (2000)
Das, M., Lerner, S., Seigle, M.: ESP: path-sensitive program verification in polynomial time. In: PLDI 2002: Programming Language Design and Implementation (2002)
Musuvathi, M.S., Park, D., Chou, A., Engler, D.R., Dill, D.L.: CMC: A pragmatic approach to model checking real code. In: OSDI 2002: Operating Systems Design and Implementation (2002)
Lahiri, S.K., Bryant, R.E.: Constructing Quantified Invariants via Predicate Abstraction. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 267–281. Springer, Heidelberg (2004)
Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855. Springer, Heidelberg (2000)
Das, S., Dill, D.L.: Successive approximation of abstract transition relations. In: Proceedings of the Sixteenth Annual IEEE Symposium on Logic in Computer Science, Boston, USA (June 2001)
Graf, S., Saïdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)
Colón, M.A., Uribe, T.E.: Generating finite-state abstractions of reactive systems using decision procedures. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 293–304. Springer, Heidelberg (1998)
Ball, T., Podelski, A., Rajamani, S.K.: Boolean and Cartesian Abstraction for Model Checking C Programs. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 268–283. Springer, Heidelberg (2001)
Harvey, W., Stuckey, P.: A unit two variable per inequality integer constraint solver for constraint logic programming. In: Australian Computer Science Conference (Australian Computer Science Communications), pp. 102–111 (1997)
Ball, T., Rajamani, S.K.: SLIC: A specification language for interface checking (of C). Technical Report MSR-TR-2001-21, Microsoft Research (2001)
Detlefs, D.L., Leino, K.R.M., Nelson, G., Saxe, J.B.: Extended static checking. Technical Report 159, Compaq Systems Research Center (1998)
Gurevich, Y., Wallace, C.: Specification and verification of the Windows Card runtime environment using abstract state machines. Technical Report MSR-TR-99-07, Microsoft Research (1999)
Cousot, P.: Abstract interpretation. Symposium on Models of Programming Languages and Computation, ACM Computing Surveys 28, 324–328 (1996)
Henzinger, T.A., Ranjit Jhala, R.M., McMillan, K.L.: Abstractions from proofs. In: In: POPL 2004: Principles of Programming Languages, pp. 232–244. ACM Press, New York (2004)
McMillan, K.L.: An Interpolating Theorem Prover. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 16–30. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cook, B., Kroening, D., Sharygina, N. (2006). Accurate Theorem Proving for Program Verification. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods. ISoLA 2004. Lecture Notes in Computer Science, vol 4313. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11925040_7
Download citation
DOI: https://doi.org/10.1007/11925040_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-48928-3
Online ISBN: 978-3-540-48929-0
eBook Packages: Computer ScienceComputer Science (R0)