Advertisement

SMT-Based Model Checking for Recursive Programs

  • Anvesh Komuravelli
  • Arie Gurfinkel
  • Sagar Chaki
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8559)

Abstract

We present an SMT-based symbolic model checking algorithm for safety verification of recursive programs. The algorithm is modular and analyzes procedures individually. Unlike other SMT-based approaches, it maintains both over- and under-approximations of procedure summaries. Under-approximations are used to analyze procedure calls without inlining. Over-approximations are used to block infeasible counterexamples and detect convergence to a proof. We show that for programs and properties over a decidable theory, the algorithm is guaranteed to find a counterexample, if one exists. However, efficiency depends on an oracle for quantifier elimination (QE). For Boolean Programs, the algorithm is a polynomial decision procedure, matching the worst-case bounds of the best BDD-based algorithms. For Linear Arithmetic (integers and rationals), we give an efficient instantiation of the algorithm by applying QE lazily. We use existing interpolation techniques to over-approximate QE and introduce Model Based Projection to under-approximate QE. Empirical evaluation on SV-COMP benchmarks shows that our algorithm improves significantly on the state-of-the-art.

Keywords

Model Check Safety Property Predicate Symbol Bounded Model Check Predicate Abstraction 
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

  1. 1.
    Albarghouthi, A., Gurfinkel, A., Chechik, M.: From Under-Approximations to Over-Approximations and Back. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 157–172. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  2. 2.
    Albarghouthi, A., Gurfinkel, A., Chechik, M.: Whale: An Interpolation-Based Algorithm for Inter-procedural Verification. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 39–55. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  3. 3.
    Albarghouthi, A., Gurfinkel, A., Li, Y., Chaki, S., Chechik, M.: UFO: Verification with Interpolants and Abstract Interpretation. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 637–640. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  4. 4.
    Alur, R., Benedikt, M., Etessami, K., Godefroid, P., Reps, T., Yannakakis, M.: Analysis of Recursive State Machines. TOPLAS 27(4), 786–818 (2005)CrossRefGoogle Scholar
  5. 5.
    Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic Predicate Abstraction of C Programs. SIGPLAN Not. 36(5), 203–213 (2001)CrossRefGoogle Scholar
  6. 6.
    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)CrossRefGoogle Scholar
  7. 7.
    Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364–387. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  8. 8.
    Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded Model Checking. Advances in Computers 58, 117–148 (2003)CrossRefGoogle Scholar
  9. 9.
    Bradley, A.R.: SAT-Based Model Checking without Unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70–87. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  10. 10.
    Chaki, S., Clarke, E.M., Groce, A., Jha, S., Veith, H.: Modular Verification of Software Components in C. IEEE Trans. Software Eng. 30(6), 388–402 (2004)CrossRefGoogle Scholar
  11. 11.
    Clarke, E.M.: Program Invariants as Fixed Points. Computing 21(4), 273–294 (1979)CrossRefMATHGoogle Scholar
  12. 12.
    Clarke, E.M.: Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems. JACM 26(1), 129–147 (1979)CrossRefMATHGoogle Scholar
  13. 13.
    Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-Guided Abstraction Refinement. In: CAV (2000)Google Scholar
  14. 14.
    Clarke, E., Kroning, 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)CrossRefGoogle Scholar
  15. 15.
    Cooper, D.C.: Theorem Proving in Arithmetic without Multiplication. In: Machine Intelligence, pp. 91–100 (1972)Google Scholar
  16. 16.
    Craig, W.: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. Symbolic Logic 22(3), 269–285 (1957)CrossRefMATHMathSciNetGoogle Scholar
  17. 17.
    de Moura, L., Bjørner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  18. 18.
    de Moura, L., Bjørner, N.S.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  19. 19.
    Esparza, J., Hansel, D., Rossmanith, P., Schwoon, S.: Efficient Algorithms for Model Checking Pushdown Systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 232–247. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  20. 20.
    Godefroid, P., Nori, A.V., Rajamani, S.K., Tetali, S.: Compositional May-Must Program Analysis: Unleashing the Power of Alternation. In: POPL, pp. 43–56 (2010)Google Scholar
  21. 21.
    Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing Software Verifiers from Proof Rules. In: PLDI, pp. 405–416 (2012)Google Scholar
  22. 22.
    Gupta, A., Ganai, M.K., Yang, Z., Ashar, P.: Iterative Abstraction using SAT-based BMC with Proof Analysis. In: ICCAD, pp. 416–423 (2003)Google Scholar
  23. 23.
    Gurfinkel, A., Wei, O., Chechik, M.: Model checking recursive programs with exact predicate abstraction. In: Cha, S(S.), Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 95–110. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  24. 24.
    Heizmann, M., Christ, J., Dietsch, D., Ermis, E., Hoenicke, J., Lindenmann, M., Nutz, A., Schilling, C., Podelski, A.: Ultimate Automizer with SMTInterpol. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 641–643. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  25. 25.
    Heizmann, M., Hoenicke, J., Podelski, A.: Nested Interpolants. SIGPLAN Not. 45(1), 471–482 (2010)CrossRefGoogle Scholar
  26. 26.
    Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proc. of POPL, pp. 58–70 (2002)Google Scholar
  27. 27.
    Hoder, K., Bjørner, N.: Generalized Property Directed Reachability. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 157–171. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  28. 28.
    Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based Model Checking for Recursive Programs. CoRR, abs/1405.4028 (2014)Google Scholar
  29. 29.
    Komuravelli, A., Gurfinkel, A., Chaki, S., Clarke, E.M.: Automatic Abstraction in SMT-Based Unbounded Software Model Checking. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 846–862. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  30. 30.
    Lal, A., Qadeer, S., Lahiri, S.K.: A solver for reachability modulo theories. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 427–443. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  31. 31.
    Loos, R., Weispfenning, V.: Applying Linear Quantifier Elimination. Computing 36(5), 450–462 (1993)MATHMathSciNetGoogle Scholar
  32. 32.
    McMillan, K.L., Amla, N.: Automatic Abstraction without Counterexamples. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 2–17. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  33. 33.
    McMillan, K.L., Rybalchenko, A.: Solving Constrained Horn Clauses using Interpolation. Technical Report MSR-TR-2013-6, Microsoft Research (2013)Google Scholar
  34. 34.
    Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT Modulo Theories: From an abstract Davis–Putnam–Logemann–Loveland procedure to DPLL(T). J. ACM 53(6), 937–977 (2006)CrossRefMathSciNetGoogle Scholar
  35. 35.
    Nipkow, T.: Linear Quantifier Elimination. J. Autom. Reason. 45(2), 189–212 (2010)CrossRefMATHMathSciNetGoogle Scholar
  36. 36.
    Reps, T.W., Horwitz, S., Sagiv, S.: Precise Interprocedural Dataflow Analysis via Graph Reachability. In: POPL, pp. 49–61 (1995)Google Scholar
  37. 37.
    Sharir, M., Pnueli, A.: Two Approaches to Interprocedural Data Flow Analysis. In: Program Flow Analysis: Theory and Applications, pp. 189–233. Prentice-Hall (1981)Google Scholar
  38. 38.
    Software Verification Competition. TACAS (2014), http://sv-comp.sosy-lab.org

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Anvesh Komuravelli
    • 1
  • Arie Gurfinkel
    • 1
  • Sagar Chaki
    • 1
  1. 1.Carnegie Mellon UniversityPittsburghUSA

Personalised recommendations