Journal of Automated Reasoning

, Volume 60, Issue 3, pp 299–335 | Cite as

A Unifying View on SMT-Based Software Verification

Article
  • 320 Downloads

Abstract

After many years of successful development of new approaches for software verification, there is a need to consolidate the knowledge about the different abstract domains and algorithms. The goal of this paper is to provide a compact and accessible presentation of four SMT-based verification approaches in order to study them in theory and in practice. We present and compare the following different “schools of thought” of software verification: bounded model checking, k-induction, predicate abstraction, and lazy abstraction with interpolants. Those approaches are well-known and successful in software verification and have in common that they are based on SMT solving as the back-end technology. We reformulate all four approaches in the unifying theoretical framework of configurable program analysis and implement them in the verification framework CPAchecker. Based on this, we can present an evaluation that thoroughly compares the different approaches, where the core differences are expressed in configuration parameters and all other variables are kept constant (such as parser front end, SMT solver, used theory in SMT formulas). We evaluate the effectiveness and the efficiency of the approaches on a large set of verification tasks and discuss the conclusions.

Keywords

Software verification Program analysis Bounded model checking k-induction Impact Lazy abstraction Predicate abstraction SMT solving 

References

  1. 1.
    Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools. Addison-Wesley, Reading, MA (1986)MATHGoogle Scholar
  2. 2.
    Albarghouthi, A., Gurfinkel, A., Chechik, M.: From under-approximations to over-approximations and back. In: Proceedings of TACAS, LNCS 7214, pp. 157–172. Springer (2012)Google Scholar
  3. 3.
    Albarghouthi, A., Li, Y., Gurfinkel, A., Chechik, M.: Ufo: A framework for abstraction- and interpolation-based software verification. In: Proceedings of CAV, LNCS 7358, pp. 672–678. Springer (2012)Google Scholar
  4. 4.
    Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: An extension of lazy abstraction with interpolation for programs with arrays. Form. Methods Syst. Des. 45(1), 63–109 (2014)CrossRefMATHGoogle Scholar
  5. 5.
    Ball, T., Cook, B., Levin, V., Rajamani, S.K.: Slam and static driver verifier: technology transfer of formal methods inside microsoft. In: Proceedings of IFM, LNCS 2999, pp. 1–20. Springer (2004)Google Scholar
  6. 6.
    Ball, T., Levin, V., Rajamani, S.K.: A decade of software model checking with SLAM. Commun. ACM 54(7), 68–76 (2011)CrossRefGoogle Scholar
  7. 7.
    Ball, T., Podelski, A., Rajamani, S.K.: Boolean and Cartesian abstraction for model checking C programs. In: Proceedings of TACAS, LNCS 2031, pp. 268–283. Springer (2001)Google Scholar
  8. 8.
    Ball, T., Rajamani, S.K.: The Slam project: debugging system software via static analysis. In: Proceedings of POPL, pp. 1–3. ACM (2002)Google Scholar
  9. 9.
    Beckert, B., Hähnle, R.: Reasoning and verification: state of the art and current trends. IEEE Intell. Syst. 29(1), 20–29 (2014)CrossRefGoogle Scholar
  10. 10.
    Beyer, D.: Software verification with validation of results (report on SV-COMP 2017). In: Proceedings of TACAS, LNCS 10206, pp. 331–349. Springer (2017)Google Scholar
  11. 11.
    Beyer, D., Cimatti, A., Griggio, A., Keremoglu, M.E., Sebastiani, R.: Software model checking via large-block encoding. In: Proceedings of FMCAD, pp. 25–32. IEEE (2009)Google Scholar
  12. 12.
    Beyer, D., Dangl, M.: SMT-based software model checking: an experimental comparison of four algorithms. In: Proceedings of VSTTE, LNCS 9971, pp. 181–198. Springer (2016)Google Scholar
  13. 13.
    Beyer, D., Dangl, M., Wendler, P.: Boosting \(k\)-induction with continuously-refined invariants. In: Proceedings of CAV, LNCS 9206, pp. 622–640. Springer (2015)Google Scholar
  14. 14.
    Beyer, D., Dangl, M., Wendler, P.: Combining \(k\)-induction with continuously-refined invariants. Technical Report MIP-1503, University of Passau (January 2015). arXiv:1502.00096
  15. 15.
    Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker Blast. Int. J. Softw. Tools Technol. Transf. 9(5–6), 505–525 (2007)CrossRefGoogle Scholar
  16. 16.
    Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Invariant synthesis for combined theories. In: Proceedings of VMCAI, LNCS 4349, pp. 378–394. Springer (2007)Google Scholar
  17. 17.
    Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Path invariants. In: Proceedings of PLDI, pp. 300–309. ACM (2007)Google Scholar
  18. 18.
    Beyer, D., Henzinger, T.A., Théoduloz, G.: Configurable software verification: concretizing the convergence of model checking and program analysis. In: Proceedings of CAV, LNCS 4590, pp. 504–518. Springer (2007)Google Scholar
  19. 19.
    Beyer, D., Henzinger, T.A., Théoduloz, G.: Program analysis with dynamic precision adjustment. In: Proceedings of ASE, pp. 29–38. IEEE (2008)Google Scholar
  20. 20.
    Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Proceedings of CAV, LNCS 6806, pp. 184–190. Springer (2011)Google Scholar
  21. 21.
    Beyer, D., Keremoglu, M.E., Wendler, P.: Predicate abstraction with adjustable-block encoding. In: Proceedings of FMCAD, pp. 189–197. FMCAD (2010)Google Scholar
  22. 22.
    Beyer, D., Löwe, S.: Explicit-state software model checking based on CEGAR and interpolation. In: Proceedings of FASE, LNCS 7793, pp. 146–162. Springer (2013)Google Scholar
  23. 23.
    Beyer, D., Löwe, S., Wendler, P.: Benchmarking and resource measurement. In: Proceedings of SPIN, LNCS 9232, pp. 160–178. Springer (2015)Google Scholar
  24. 24.
    Beyer, D., Petrenko, A.K.: Linux driver verification. In: Proceedings of ISoLA, LNCS 7610, pp. 1–6. Springer (2012)Google Scholar
  25. 25.
    Beyer, D., Wendler, P.: Algorithms for software model checking: predicate abstraction vs. Impact. In: Proceedings of FMCAD, pp. 106–113. FMCAD (2012)Google Scholar
  26. 26.
    Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Proceedings of TACAS, LNCS 1579, pp. 193–207. Springer (1999)Google Scholar
  27. 27.
    Birgmeier, J., Bradley, A.R., Weissenbacher, G.: Counterexample to induction-guided abstraction-refinement (CTIGAR). In: Proceedings of CAV, LNCS 8559, pp. 831–848. Springer (2014)Google Scholar
  28. 28.
    Bradley, A.R.: SAT-based model checking without unrolling. In: Proceedings of VMCAI, LNCS 6538, pp. 70–87. Springer (2011)Google Scholar
  29. 29.
    Brain, M., Joshi, S., Kröning, D., Schrammel, P.: Safety verification and refutation by \(k\)-invariants and \(k\)-induction. In: Proceedings of SAS, LNCS 9291, pp. 145–161. Springer (2015)Google Scholar
  30. 30.
    Brückner, I., Dräger, K., Finkbeiner, B., Wehrheim, H.: Slicing abstractions. Fundam. Inform. 89(4), 369–392 (2008)MathSciNetMATHGoogle Scholar
  31. 31.
    Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. 35(8), 677–691 (1986)CrossRefMATHGoogle Scholar
  32. 32.
    Cimatti, A., Griggio, A.: Software model checking via IC3. In: Proceedings of CAV, LNCS 7358, pp. 277–293. Springer (2012)Google Scholar
  33. 33.
    Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: IC3 modulo theories via implicit predicate abstraction. In: Proceedings of TACAS, LNCS 8413, pp. 46–61. Springer (2014)Google Scholar
  34. 34.
    Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752–794 (2003)MathSciNetCrossRefMATHGoogle Scholar
  35. 35.
    Clarke, E.M., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Proceedings of TACAS, LNCS 2988, pp. 168–176. Springer (2004)Google Scholar
  36. 36.
    Colón, M., Sankaranarayanan, S., Sipma, H.B.: Linear invariant generation using non-linear constraint solving. In: Proceedings of CAV, LNCS 2725, pp. 420–432. Springer (2003)Google Scholar
  37. 37.
    Cordeiro, L.C., Morse, J., Nicole, D., Fischer, B.: Context-bounded model checking with Esbmc 1.17 (competition contribution). In: Proceedings of TACAS, LNCS 7214, pp. 534–537. Springer (2012)Google Scholar
  38. 38.
    Craig, W.: Linear reasoning. A new form of the Herbrand–Gentzen theorem. J. Symb. Log. 22(3), 250–268 (1957)MathSciNetCrossRefMATHGoogle Scholar
  39. 39.
    Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Efficiently computing static single assignment form and the control dependence graph. ACM Trans. Program. Lang. Syst. 13(4), 451–490 (1991)CrossRefGoogle Scholar
  40. 40.
    Dillig, I., Dillig, T., Li, B., McMillan, K.L.: Inductive invariant generation via abductive inference. In: Proceedings of OOPSLA, pp. 443–456. ACM (2013)Google Scholar
  41. 41.
    Donaldson, A.F., Haller, L., Kroening, D., Rümmer, P.: Software verification using \(k\)-induction. In: Proceedings of SAS, LNCS 6887, pp. 351–368. Springer (2011)Google Scholar
  42. 42.
    Eén, N., Mishchenko, A., Brayton, R.K.: Efficient implementation of property directed reachability. In: Proceedings of FMCAD, pp. 125–134. FMCAD Inc. (2011)Google Scholar
  43. 43.
    Ermis, E., Hoenicke, J., Podelski, A.: Splitting via interpolants. In: Proceedings of VMCAI, LNCS 7148, pp. 186–201. Springer (2012)Google Scholar
  44. 44.
    Gadelha, M.Y.R., Ismail, H.I., Cordeiro, L.C.: Handling loops in bounded model checking of C programs via \(k\)-induction. Int. J. Softw. Tools Technol. Transf. 19(1), 97–114 (2017)CrossRefGoogle Scholar
  45. 45.
    Ghilardi, S., Ranise, S.: Goal-directed invariant synthesis for model checking modulo theories. In: Proceedings of TABLEAUX, LNCS 5607, pp. 173–188. Springer (2009)Google Scholar
  46. 46.
    Ghilardi, S., Ranise, S.: Backward reachability of array-based systems by SMT solving: termination and invariant synthesis. Log. Methods Comput. Sci. 6(4) (2010)Google Scholar
  47. 47.
    Graf, S., Saïdi, H.: Construction of abstract state graphs with Pvs. In: Proceedings of CAV, LNCS 1254, pp. 72–83. Springer (1997)Google Scholar
  48. 48.
    Gurfinkel, A., Kahsai, T., Navas, J.A.: SeaHorn: a framework for verifying C programs (competition contribution). In: Proceedings of TACAS, LNCS 9035, pp. 447–450. Springer (2015)Google Scholar
  49. 49.
    Hajdu, Á., Tóth, T., Vörös, A., Majzik, I.: A configurable CEGAR framework with interpolation-based refinements. In: Proceedings of FORTE, LNCS 9688, pp. 158–174. Springer (2016)Google Scholar
  50. 50.
    Heizmann, M., Hoenicke, J., Podelski, A.: Refinement of trace abstraction. In: Proceedings of SAS, LNCS 5673, pp. 69–85. Springer (2009)Google Scholar
  51. 51.
    Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proceedings of POPL, pp. 58–70. ACM (2002)Google Scholar
  52. 52.
    Hoder, K., Bjørner, N.: Generalized property directed reachability. In: Proceedings of SAT, LNCS 7317, pp. 157–171. Springer (2012)Google Scholar
  53. 53.
    Jhala, R., Majumdar, R.: Software model checking. ACM Comput. Surv. 41(4), 21:1–21:54 (2009)CrossRefGoogle Scholar
  54. 54.
    Jovanovic, D., Dutertre, B.: Property-directed \(k\)-induction. In: Proceedings of FMCAD, pp. 85–92. IEEE (2016)Google Scholar
  55. 55.
    Kahsai, T., Tinelli, C.: PKind: a parallel \(k\)-induction based model checker. In: Proceedings of International Workshop on Parallel and Distributed Methods in Verification, EPTCS 72, pp. 55–62 (2011)Google Scholar
  56. 56.
    Khoroshilov, A.V., Mutilin, V.S., Petrenko, A.K., Zakharov, V.: Establishing Linux driver verification process. In: Proceedings of Ershov Memorial Conference, LNCS 5947, pp. 165–176. Springer (2009)Google Scholar
  57. 57.
    Kildall, G.A.: A unified approach to global program optimization. In: Proceedings of POPL, pp. 194–206. ACM (1973)Google Scholar
  58. 58.
    King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385–394 (1976)MathSciNetCrossRefMATHGoogle Scholar
  59. 59.
    Komuravelli, A., Gurfinkel, A., Chaki, S., Clarke, E.M.: Automatic abstraction in SMT-based unbounded software model checking. In: Proceedings of CAV, LNCS 8044, pp. 846–862. Springer (2013)Google Scholar
  60. 60.
    McMillan, K.L.: Interpolation and SAT-based model checking. In: Proceedings of CAV, LNCS 2725, pp. 1–13. Springer (2003)Google Scholar
  61. 61.
    McMillan, K.L.: Lazy abstraction with interpolants. In: Proceedings of CAV, LNCS 4144, pp. 123–136. Springer (2006)Google Scholar
  62. 62.
    McMillan, K.L., Amla, N.: Automatic abstraction without counterexamples. In: Proceedings of TACAS, LNCS 2619, pp. 2–17. Springer (2003)Google Scholar
  63. 63.
    Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Berlin (1999)CrossRefMATHGoogle Scholar
  64. 64.
    Rakamarić, Z., Emmi, M.: SMACK: decoupling source language details from verifier implementations. In: Proceedings of CAV, LNCS 8559, pp. 106–113. Springer (2014)Google Scholar
  65. 65.
    Rocha, H., Ismail, H.I., Cordeiro, L.C., Barreto, R.S.: Model checking embedded C software using \(k\)-induction and invariants. In: Proceedings of SBESC, pp. 90–95. IEEE (2015)Google Scholar
  66. 66.
    Schrammel, P., Kroening, D.: 2LS for program analysis (competition contribution). In: Proceedings of TACAS, LNCS 9636, pp. 905–907. Springer (2016)Google Scholar
  67. 67.
    Schuppan, V., Biere, A.: Liveness checking as safety checking for infinite state spaces. Electron. Notes Theor. Comput. Sci. 149(1), 79–96 (2006)MathSciNetCrossRefMATHGoogle Scholar
  68. 68.
    Sheeran, M., Singh, S., Stålmarck, G.: Checking safety properties using induction and a SAT-solver. In: Proceedings of FMCAD, LNCS 1954, pp. 127–144. Springer (2000)Google Scholar
  69. 69.
    Sinz, C., Merz, F., Falke, S.: Llbmc: A bounded model checker for Llvm’s intermediate representation (competition contribution). In: Proceedings of TACAS, LNCS 7214, pp. 542–544. Springer (2012)Google Scholar
  70. 70.
    Wahl, T.: The \(k\)-induction principle. Available at http://www.ccs.neu.edu/home/wahl/Publications/k-induction.pdf (2013)
  71. 71.
    Wendler, P.: CPAchecker with sequential combination of explicit-state analysis and predicate analysis (competition contribution). In: Proceedings of TACAS, LNCS 7795, pp. 613–615. Springer (2013)Google Scholar

Copyright information

© Springer Science+Business Media B.V. 2017

Authors and Affiliations

  1. 1.LMU MunichMunichGermany

Personalised recommendations