Abstract
Symbolic execution with interpolation is emerging as an alternative to cegar for software verification. The performance of both methods relies critically on interpolation in order to obtain the most general abstraction of the current symbolic or abstract state which can be shown to remain error-free. cegar naturally handles unbounded loops because it is based on abstract interpretation. In contrast, symbolic execution requires a special extension for such loops.
In this paper, we present such an extension. Its main characteristic is that it performs eager subsumption, that is, it always attempts to perform abstraction in order to avoid exploring redundant symbolic states. It balances this primary desire for more abstraction with the secondary desire to maintain the strongest loop invariant, for earlier detection of infeasible paths, which entails less abstraction. Occasionally certain abstractions are not permitted because of the reachability of error states; this is the underlying mechanism which then causes selective unrolling, that is, the unrolling of a loop along relevant paths only.
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.
References
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)
Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic Predicate Abstraction of C Programs. In: PLDI 2001, pp. 203–213 (2001)
Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. The KeY Approach. LNCS (LNAI), vol. 4334, pp. 375–405. Springer, Heidelberg (2007)
Beckman, N.E., Nori, A.V., Rajamani, S.K., Simmons, R.J.: Proofs from Tests. In: ISSTA 2008, pp. 3–14 (2008)
Beyer, D., Cimatti, A., Griggio, A., Keremoglu, M.E., Sebastiani, R.: Software Model Checking via Large-Block Encoding. In: FMCAD 2009 (2009)
Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Path Invariants. In: PLDI 2007, pp. 300–309 (2007)
Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The Software Model Checker BLAST. Int. J. STTT 9, 505–525 (2007)
Cadar, C., Ganesh, V., Pawlowski, P.M., Dill, D.L., Engler, D.R.: Exe: Automatically Generating Inputs of Death. In: CCS 2006, pp. 322–335 (2006)
Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: CounterrExample-Guided Abstraction Refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, Springer, Heidelberg (2000)
Craig, W.: Three uses of Herbrand-Gentzen theorem in relating model theory and proof theory. Journal of Symbolic Computation 22 (1955)
Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall (1976)
Godefroid, P., Klarlund, N., Sen, K.: DART: Directed Automated Random Testing. In: PLDI 2005, pp. 213–223 (2005)
Godefroid, P., Nori, A.V., Rajamani, S.K., Tetali, S.D.: Compositional must program analysis: unleashing the power of alternation. In: POPL 2010, pp. 43–56 (2010)
Gulavani, B.S., Henzinger, T.A., Kannan, Y., Nori, A.V., Rajamani, S.K.: Synergy: A New Algorithm for Property Checking. In: SIGSOFT 2006/FSE-14, pp. 117–127 (2006)
Harris, W.R., Sankaranarayanan, S., Ivančić, F., Gupta, A.: Program Analysis via Satisfiability Modulo Path Programs. In: POPL 2010, pp. 71–82 (2010)
Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from Proofs. In: POPL 2004, pp. 232–244 (2004)
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy Abstraction. In: POPL 2002 (2002)
Jacobs, B., Piessens, F.: The Verifast Program Verifier (2008)
Jaffar, J., et al.: The CLP(R) Language and System. ACM TOPLAS 14(3), 339–395 (1992)
Jaffar, J., Santosa, A.E., Voicu, R.: Efficient Memoization for Dynamic Programming with Ad-hoc Constraints. In: AAAI 2008, pp. 297–303 (2008)
Jaffar, J., Santosa, A.E., Voicu, R.: An Interpolation Method for CLP Traversal. In: Gent, I.P. (ed.) CP 2009. LNCS, vol. 5732, pp. 454–469. Springer, Heidelberg (2009)
King, J.C.: Symbolic Execution and Program Testing. Com. ACM, 385–394 (1976)
McMillan, K.L.: Lazy Abstraction with Interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 123–136. Springer, Heidelberg (2006)
McMillan, K.L.: Lazy Annotation for Program Testing and Verification. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 104–118. Springer, Heidelberg (2010)
Podelski, A., Rybalchenko, A.: ARMC: The Logical Choice for Software Model Checking with Abstraction Refinement. In: Hanus, M. (ed.) PADL 2007. LNCS, vol. 4354, pp. 245–259. Springer, Heidelberg (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jaffar, J., Navas, J.A., Santosa, A.E. (2012). Unbounded Symbolic Execution for Program Verification. In: Khurshid, S., Sen, K. (eds) Runtime Verification. RV 2011. Lecture Notes in Computer Science, vol 7186. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-29860-8_32
Download citation
DOI: https://doi.org/10.1007/978-3-642-29860-8_32
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-29859-2
Online ISBN: 978-3-642-29860-8
eBook Packages: Computer ScienceComputer Science (R0)