Advertisement

SAT-Based Model Checking

  • Armin Biere
  • Daniel Kröning
Chapter

Abstract

Modern satisfiability (SAT) solvers have become the enabling technology of many model checkers. In this chapter, we will focus on those techniques most relevant to industrial practice. In bounded model checking (BMC), a transition system and a property are jointly unwound for a given number \(k\) of steps to obtain a formula that is satisfiable if there is a counterexample for the property up to length \(k\). The formula is then passed to an efficient SAT solver. The strength of BMC is refutation: BMC has been used to discover subtle flaws in digital systems. We cover the application of BMC to both hardware and software systems, and to hardware/software co-verification. We also discuss means to make BMC complete, including \(k\)-induction, Craig interpolation, abstraction refinement techniques, and inductive techniques with iterative strengthening.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Abdulla, P.A., Bjesse, P., Eén, N.: Symbolic reachability analysis based on SAT-solvers. In: Graf, S., Schwartzbach, M.I. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 1785, pp. 411–425. Springer, Heidelberg (2000) zbMATHGoogle Scholar
  2. 2.
    Alglave, J., Kroening, D., Tautschnig, M.: Partial orders for efficient bounded model checking of concurrent software. In: Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 8044, pp. 141–157. Springer, Heidelberg (2013) CrossRefGoogle Scholar
  3. 3.
    Alpern, B., Wegman, M.N., Zadeck, F.K.: Detecting equality of variables in programs. In: Ferrante, J., Mager, P. (eds.) Symp. on Principles of Programming Languages (POPL), pp. 1–11. ACM, New York (1988) Google Scholar
  4. 4.
    Amla, N., McMillan, K.L.: A hybrid of counterexample-based and proof-based abstraction. In: Hu, A.J., Martin, A.K. (eds.) Formal Methods in Computer Aided Design (FMCAD). LNCS, vol. 3312, pp. 260–274. Springer, Heidelberg (2004) CrossRefGoogle Scholar
  5. 5.
    Awedh, M., Somenzi, F.: Proving more properties with bounded model checking. In: Alur, R., Peled, D. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 3114, pp. 96–108. Springer, Heidelberg (2004) CrossRefGoogle Scholar
  6. 6.
    Awedh, M., Somenzi, F.: Automatic invariant strengthening to prove properties in bounded model checking. In: Sentovich, E. (ed.) Design Automation Conf. (DAC), pp. 1073–1076. ACM, New York (2006) Google Scholar
  7. 7.
    Awedh, M., Somenzi, F.: Termination criteria for bounded model checking: extensions and comparison. Electron. Notes Theor. Comput. Sci. 144(1), 51–66 (2006) zbMATHCrossRefGoogle Scholar
  8. 8.
    Ball, T., Bounimova, E., Cook, B., Levin, V., Lichtenberg, J., McGarvey, C., Ondrusek, B., Rajamani, S.K., Ustuner, A.: Thorough static analysis of device drivers. In: Berbers, Y., Zwaenepoel, W. (eds.) European Conf. on Computer Systems (EuroSys), pp. 73–85. ACM, New York (2006) Google Scholar
  9. 9.
    Ball, T., Bounimova, E., Kumar, R., Levin, V.: SLAM2: Static driver verification with under 4% false alarms. In: Bloem, R., Sharygina, N. (eds.) Formal Methods in Computer Aided Design (FMCAD), pp. 35–42. IEEE, Piscataway (2010) Google Scholar
  10. 10.
    Ball, T., Cook, B., Lahiri, S.K., Zhang, L.: Zapato: automatic theorem proving for predicate abstraction refinement. In: Alur, R., Peled, D. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 3114, pp. 457–461. Springer, Heidelberg (2004) CrossRefGoogle Scholar
  11. 11.
    Ball, T., Podelski, A., Rajamani, S.K.: Boolean and Cartesian abstraction for model checking C programs. In: Margaria, T., Yi, W. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 2031, pp. 268–283. Springer, Heidelberg (2001) Google Scholar
  12. 12.
    Ball, T., Rajamani, S.K.: Bebop: a symbolic model checker for boolean programs. In: Havelund, K., Penix, J., Visser, W. (eds.) Intl. Workshop on SPIN Model Checking and Software Verification. LNCS, vol. 1885, pp. 113–130. Springer, Heidelberg (2000) CrossRefGoogle Scholar
  13. 13.
    Ball, T., Rajamani, S.K.: Boolean programs: a model and process for software analysis. Tech. rep., Microsoft Research (2000) Google Scholar
  14. 14.
    Barner, S., Eisner, C., Glazberg, Z., Kroening, D., Rabinovitz, I.: ExpliSAT: guiding SAT-based software verification with explicit states. In: Yorav, K. (ed.) Intl. Haifa Verification Conference (HVC). LNCS, vol. 4383, pp. 138–154. Springer, Heidelberg (2007) Google Scholar
  15. 15.
    Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 825–885. IOS Press, Amsterdam (2009) Google Scholar
  16. 16.
    Barrett, C.W., Tinelli, C.: Satisfiability modulo theories. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018) Google Scholar
  17. 17.
    Basler, G., Kroening, D., Weissenbacher, G.: SAT-based summarization for Boolean programs. In: Bosnacki, D., Edelkamp, S. (eds.) Intl. Workshop on Model Checking Software (SPIN). LNCS, vol. 4595, pp. 131–148 (2007) CrossRefGoogle Scholar
  18. 18.
    Basler, G., Mazzucchi, M., Wahl, T., Kroening, D.: Symbolic counter abstraction for concurrent software. In: Bouajjani, A., Maler, O. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 5643, pp. 64–78. Springer, Heidelberg (2009) CrossRefGoogle Scholar
  19. 19.
    Basler, G., Mazzucchi, M., Wahl, T., Kroening, D.: Context-aware counter abstraction. Form. Methods Syst. Des. 36(3), 223–245 (2010) zbMATHCrossRefGoogle Scholar
  20. 20.
    Baumgartner, J., Kuehlmann, A.: Enhanced diameter bounding via structural transformation. In: Design, Automation & Test in Europe Conf. and Exposition (DATE), pp. 36–41. IEEE, Piscataway (2004) CrossRefGoogle Scholar
  21. 21.
    Baumgartner, J., Kuehlmann, A., Abraham, J.A.: Property checking via structural analysis. In: Brinksma, E., Larsen, K.G. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 2404, pp. 151–165. Springer, Heidelberg (2002) CrossRefGoogle Scholar
  22. 22.
    Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Invariant synthesis for combined theories. In: Cook, B., Podelski, A. (eds.) Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI). LNCS, vol. 4349, pp. 378–394. Springer, Heidelberg (2007) CrossRefGoogle Scholar
  23. 23.
    Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Path invariants. In: Ferrante, J., McKinley, K.S. (eds.) Conf. on Programming Language Design and Implementation (PLDI), pp. 300–309. ACM, New York (2007) Google Scholar
  24. 24.
    Biere, A.: Bounded model checking. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 457–481. IOS Press, Amsterdam (2009) Google Scholar
  25. 25.
    Biere, A., Artho, C., Schuppan, V.: Liveness checking as safety checking. In: Cleaveland, R., Garavel, H. (eds.) Intl. ERCIM Workshop on Formal Methods for Industrial Critical Systems (FMICS), pp. 160–177. Elsevier, Amsterdam (2002) Google Scholar
  26. 26.
    Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, R. (ed.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999) Google Scholar
  27. 27.
    Biere, A., Heljanko, K., Junttila, T.A., Latvala, T., Schuppan, V.: Linear encodings of bounded LTL model checking. Log. Methods Comput. Sci. 2(5), 1–64 (2006) MathSciNetzbMATHCrossRefGoogle Scholar
  28. 28.
    Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press, Amsterdam (2009) zbMATHGoogle Scholar
  29. 29.
    Blanc, N., Kroening, D.: Race analysis for SystemC using model checking. In: Intl. Conf. on Computer-Aided Design (ICCAD), pp. 356–363. IEEE, Piscataway (2008) Google Scholar
  30. 30.
    Blanc, N., Kroening, D.: Race analysis for SystemC using model checking. ACM Trans. Des. Autom. Electron. Syst. 15(3), 1–32 (2010) CrossRefGoogle Scholar
  31. 31.
    Blanc, N., Kroening, D., Sharygina, N.: Scoot: a tool for the analysis of SystemC models. In: Ramakrishnan, C.R., Rehof, J. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 4963, pp. 467–470. Springer, Heidelberg (2008) Google Scholar
  32. 32.
    Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: application to model-checking. In: Mazurkiewicz, A.W., Winkowski, J. (eds.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol. 1243, pp. 135–150. Springer, Heidelberg (1997) CrossRefGoogle Scholar
  33. 33.
    Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D.A. (eds.) Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI). LNCS, vol. 6538, pp. 70–87. Springer, Heidelberg (2011) CrossRefGoogle Scholar
  34. 34.
    Bradley, A.R.: Understanding IC3. In: Cimatti, A., Sebastiani, R. (eds.) Theory and Applications of Satisfiability Testing (SAT). LNCS, vol. 7317, pp. 1–14. Springer, Heidelberg (2012) Google Scholar
  35. 35.
    Bradley, A.R., Manna, Z.: Checking safety by inductive generalization of counterexamples to induction. In: Formal Methods in Computer Aided Design (FMCAD), pp. 173–180. IEEE, Piscataway (2007) CrossRefGoogle Scholar
  36. 36.
    Brillout, A., Kroening, D., Rümmer, P., Wahl, T.: An interpolating sequent calculus for quantifier-free Presburger arithmetic. In: Giesl, J., Hähnle, R. (eds.) Intl. Joint Conf. on Automated Reasoning (IJCAR). LNCS, vol. 6173, pp. 384–399. Springer, Heidelberg (2010) CrossRefGoogle Scholar
  37. 37.
    Brillout, A., Kroening, D., Rümmer, P., Wahl, T.: Beyond quantifier-free interpolation in extensions of Presburger arithmetic. In: Jhala, R., Schmidt, D.A. (eds.) Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI). LNCS, vol. 6538, pp. 88–102. Springer, Heidelberg (2011) CrossRefGoogle Scholar
  38. 38.
    Brillout, A., Kroening, D., Wahl, T.: Mixed abstractions for floating-point arithmetic. In: Formal Methods in Computer Aided Design (FMCAD), pp. 69–76. IEEE, Piscataway (2009) Google Scholar
  39. 39.
    Brummayer, R., Biere, A.: Effective bit-width and under-approximation. In: Moreno-Díaz, R., Pichler, F., Quesada-Arencibia, A. (eds.) Intl. Conf. on Computer Aided Systems Theory (EUROCAST). LNCS, vol. 5717, pp. 304–311. Springer, Heidelberg (2009) Google Scholar
  40. 40.
    Bryant, R.E.: Graph Based Algorithms for Boolean Function Manipulation. Trans. Comput. C-35(8), 677–691 (1986) zbMATHCrossRefGoogle Scholar
  41. 41.
    Bryant, R.E., Kroening, D., Ouaknine, J., Seshia, S.A., Strichman, O., Brady, B.: Deciding bit-vector arithmetic with abstraction. In: Grumberg, O., Huth, M. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 4424, pp. 358–372. Springer, Heidelberg (2007) Google Scholar
  42. 42.
    Büchi, J.R.: Regular canonical systems. Arch. Math. Log. 6(3–4), 91–111 (1964) MathSciNetzbMATHGoogle Scholar
  43. 43.
    Cadar, C., Sen, K.: Symbolic execution for software testing: Three decades later. Commun. ACM 56(2), 82–90 (2013) CrossRefGoogle Scholar
  44. 44.
    Case, M.L., Mony, H., Baumgartner, J., Kanzelman, R.: Enhanced verification by temporal decomposition. In: Formal Methods in Computer Aided Design (FMCAD), pp. 17–24. IEEE, Piscataway (2009) Google Scholar
  45. 45.
    Chambers, B., Manolios, P., Vroon, D.: Faster SAT solving with better CNF generation. In: Design, Automation & Test in Europe (DATE), pp. 1590–1595. IEEE, Piscataway (2009) Google Scholar
  46. 46.
    Chauhan, P., Clarke, E.M., Kroening, D.: A SAT-based algorithm for reparameterization in symbolic simulation. In: Malik, S., Fix, L., Kahng, A.B. (eds.) Design Automation Conf. (DAC), pp. 524–529. ACM, New York (2004) Google Scholar
  47. 47.
    Chockler, H., Kroening, D., Purandare, M.: Computing mutation coverage in interpolation-based model checking. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. 31(5), 765–778 (2012) CrossRefGoogle Scholar
  48. 48.
    Cimatti, A., Griggio, A.: Software model checking via IC3. In: Madhusudan, P., Seshia, S.A. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 7358, pp. 277–293. Springer, Heidelberg (2012) CrossRefGoogle Scholar
  49. 49.
    Claessen, K., Sörensson, N.: A liveness checking algorithm that counts. In: Cabodi, G., Singh, S. (eds.) Formal Methods in Computer Aided Design (FMCAD), pp. 52–59. IEEE, Piscataway (2012) Google Scholar
  50. 50.
    Clarke, E., Jain, H., Kroening, D.: Verification of SpecC using predicate abstraction. Form. Methods Syst. Des. 30(1), 5–28 (2007) zbMATHCrossRefGoogle Scholar
  51. 51.
    Clarke, E., Kroening, D.: Hardware verification using ANSI-C programs as a reference. In: Yasuura, H. (ed.) Asia and South Pacific Design Automation Conf. (ASPDAC), pp. 308–311. IEEE, Piscataway (2003) Google Scholar
  52. 52.
    Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004) Google Scholar
  53. 53.
    Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: Predicate abstraction of ANSI-C programs using SAT. Form. Methods Syst. Des. 25(2–3), 105–127 (2004) zbMATHCrossRefGoogle Scholar
  54. 54.
    Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: SATABS: SAT-based predicate abstraction for ANSI-C. In: Halbwachs, N., Zuck, L.D. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 3440, pp. 570–574. Springer, Heidelberg (2005) zbMATHGoogle Scholar
  55. 55.
    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) MathSciNetzbMATHCrossRefGoogle Scholar
  56. 56.
    Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. Trans. Program. Lang. Syst. 16(5), 1512–1542 (1994) CrossRefGoogle Scholar
  57. 57.
    Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999) Google Scholar
  58. 58.
    Clarke, E.M., Kroening, D., Ouaknine, J., Strichman, O.: Computational challenges in bounded model checking. Softw. Tools Technol. Transf. 7(2), 174–183 (2005) CrossRefGoogle Scholar
  59. 59.
    Cook, B., Kroening, D., Sharygina, N.: Cogent: accurate theorem proving for program verification. In: Etessami, K., Rajamani, S.K. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 3576, pp. 296–300. Springer, Heidelberg (2005) zbMATHCrossRefGoogle Scholar
  60. 60.
    Cordeiro, L., Fischer, B.: Verifying multi-threaded software using SMT-based context-bounded model checking. In: Taylor, R.N., Gall, H., Medvidovic, N. (eds.) Intl. Conf. on Software Engineering (ICSE), pp. 331–340. ACM, New York (2011) Google Scholar
  61. 61.
    Cotton, S.: Natural domain SMT: a preliminary assessment. In: Chatterjee, K., Henzinger, T.A. (eds.) Intl. Conf. on Formal Modeling and Analysis of Timed Systems (FORMATS). LNCS, vol. 6246, pp. 77–91. Springer, Heidelberg (2010) CrossRefGoogle Scholar
  62. 62.
    Currie, D.W., Hu, A.J., Rajan, S.P.: Automatic formal verification of DSP software. In: Micheli, G.D. (ed.) Design Automation Conf. (DAC), pp. 130–135. ACM, New York (2000) Google Scholar
  63. 63.
    Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. Tech. rep., HP Labs (2003) Google Scholar
  64. 64.
    Donaldson, A., Haller, L., Kroening, D.: Strengthening induction-based race checking with lightweight static analysis. In: Jhala, R., Schmidt, D.A. (eds.) Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI). LNCS, vol. 6538, pp. 169–183. Springer, Heidelberg (2011) CrossRefGoogle Scholar
  65. 65.
    Donaldson, A., Kroening, D., Rümmer, P.: Automatic analysis of scratch-pad memory code for heterogeneous multicore processors. In: Esparza, J., Majumdar, R. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 6015, pp. 280–295. Springer, Heidelberg (2010) Google Scholar
  66. 66.
    D’Silva, V., Haller, L., Kroening, D.: Satisfiability solvers are static analysers. In: Miné, A., Schmidt, D. (eds.) Intl. Symp. on Static Analysis (SAS). LNCS, vol. 7460, pp. 317–333. Springer, Heidelberg (2012) CrossRefGoogle Scholar
  67. 67.
    D’Silva, V., Haller, L., Kroening, D.: Abstract conflict driven learning. In: Giacobazzi, R., Cousot, R. (eds.) Symp. on Principles of Programming Languages (POPL), pp. 143–154. ACM, New York (2013) Google Scholar
  68. 68.
    D’Silva, V., Haller, L., Kroening, D., Tautschnig, M.: Numeric bounds analysis with conflict-driven learning. In: Flanagan, C., König, B. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 7214, pp. 48–63. Springer, Berlin (2012) zbMATHGoogle Scholar
  69. 69.
    D’Silva, V., Kroening, D., Weissenbacher, G.: A survey of automated techniques for formal software verification. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. 27(7), 1165–1178 (2008) CrossRefGoogle Scholar
  70. 70.
    Dubrovin, J., Junttila, T.A., Heljanko, K.: Exploiting step semantics for efficient bounded model checking of asynchronous systems. Sci. Comput. Program. 77(10–11), 1095–1121 (2012) zbMATHCrossRefGoogle Scholar
  71. 71.
    Eén, N., Mishchenko, A., Brayton, R.K.: Efficient implementation of property directed reachability. In: Bjesse, P., Slobodová, A. (eds.) Formal Methods in Computer Aided Design (FMCAD), pp. 125–134. FMCAD, Austin (2011) Google Scholar
  72. 72.
    Eén, N., Mishchenko, A., Sörensson, N.: Applying logic synthesis for speeding up SAT. In: Marques-Silva, J., Sakallah, K.A. (eds.) Theory and Applications of Satisfiability Testing (SAT). LNCS, vol. 4501, pp. 272–286. Springer, Heidelberg (2007) zbMATHGoogle Scholar
  73. 73.
    Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) Theory and Applications of Satisfiability Testing (SAT). LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2003) zbMATHCrossRefGoogle Scholar
  74. 74.
    Eén, N., Sterin, B., Claessen, K.: A circuit approach to LTL model checking. In: Jobstmann, B., Ray, S. (eds.) Formal Methods in Computer Aided Design (FMCAD), pp. 53–60. IEEE, Piscataway (2013) Google Scholar
  75. 75.
    van Eijk, C.A.J.: Sequential equivalence checking based on structural similarities. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. 19(7), 814–819 (2000) CrossRefGoogle Scholar
  76. 76.
    Eisner, C., Fisman, D.: A Practical Introduction to PSL. Springer, Heidelberg (2006) Google Scholar
  77. 77.
    Eisner, C., Fisman, D.: Functional specification of hardware via temporal logic. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018) zbMATHGoogle Scholar
  78. 78.
    Emmi, M., Qadeer, S., Rakamaric, Z.: Delay-bounded scheduling. In: Ball, T., Sagiv, M. (eds.) Symp. on Principles of Programming Languages (POPL), pp. 411–422. ACM, New York (2011) Google Scholar
  79. 79.
    Finkel, A., Willems, B., Wolper, P.: A direct symbolic approach to model checking pushdown systems. Electron. Notes Theor. Comput. Sci. 9, 27–37 (1997) zbMATHCrossRefGoogle Scholar
  80. 80.
    Gan, X., Dubrovin, J., Heljanko, K.: A symbolic model checking approach to verifying satellite onboard software. Sci. Comput. Program. 82, 44–55 (2014) CrossRefGoogle Scholar
  81. 81.
    Ganai, M.K., Gupta, A.: SAT-Based Scalable Formal Verification Solutions. Springer, Heidelberg (2007) zbMATHCrossRefGoogle Scholar
  82. 82.
    Ghafari, N., Hu, A.J., Rakamaric, Z.: Context-bounded translations for concurrent software: an empirical evaluation. In: van de Pol, J., Weber, M. (eds.) Intl. Workshop on Model Checking Software (SPIN). LNCS, vol. 6349, pp. 227–244. Springer, Heidelberg (2010) CrossRefGoogle Scholar
  83. 83.
    Giunchiglia, E., Marin, P., Narizzano, M.: Reasoning with quantified boolean formulas. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 761–780. IOS Press, Amsterdam (2009) Google Scholar
  84. 84.
    Graf, S., Saïdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997) CrossRefGoogle Scholar
  85. 85.
    Groce, A., Kroening, D.: Making the most of BMC counterexamples. Electron. Notes Theor. Comput. Sci. 119, 67–81 (2005) zbMATHCrossRefGoogle Scholar
  86. 86.
    Groce, A., Kroening, D., Clarke, E.: Counterexample guided abstraction refinement via program execution. In: Davies, J., Schulte, W., Barnett, M. (eds.) Intl. Conf. on Formal Engineering Methods (ICFEM). LNCS, vol. 3308, pp. 224–238. Springer, Heidelberg (2004) Google Scholar
  87. 87.
    Groce, A., Kroening, D., Lerda, F.: Understanding counterexamples with explain. In: Alur, R., Peled, D.A. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 3114, pp. 453–456. Springer, Heidelberg (2004) CrossRefGoogle Scholar
  88. 88.
    Gupta, A., Kahlon, V., Qadeer, S., Touili, T.: Model checking concurrent programs. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018) zbMATHGoogle Scholar
  89. 89.
    Hassan, Z., Bradley, A.R., Somenzi, F.: Incremental, inductive CTL model checking. In: Madhusudan, P., Seshia, S.A. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 7358, pp. 532–547. Springer, Heidelberg (2012) CrossRefGoogle Scholar
  90. 90.
    Heljanko, K., Junttila, T.A., Keinänen, M., Lange, M., Latvala, T.: Bounded model checking for weak alternating Büchi automata. In: Ball, T., Jones, R.B. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 4144, pp. 95–108. Springer, Heidelberg (2006) CrossRefGoogle Scholar
  91. 91.
    Heljanko, K., Junttila, T.A., Latvala, T.: Incremental and complete bounded model checking for full PLTL. In: Etessami, K., Rajamani, S.K. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 3576, pp. 98–111. Springer, Heidelberg (2005) CrossRefGoogle Scholar
  92. 92.
    Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: Jones, N.D., Leroy, X. (eds.) Symp. on Principles of Programming Languages (POPL), pp. 232–244. ACM, New York (2004) Google Scholar
  93. 93.
    Hoder, K., Bjørner, N.: Generalized property directed reachability. In: Cimatti, A., Sebastiani, R. (eds.) Theory and Applications of Satisfiability Testing (SAT). LNCS, vol. 7317, pp. 157–171. Springer, Heidelberg (2012) Google Scholar
  94. 94.
    Ivancic, F., Shlyakhter, I., Gupta, A., Ganai, M.K.: Model checking C programs using F-SOFT. In: Intl. Conf. on Computer Design (ICCD), pp. 297–308. IEEE, Piscataway (2005) Google Scholar
  95. 95.
    Jain, H., Clarke, E.M.: Efficient SAT solving for non-clausal formulas using DPLL, graphs, and watched cuts. In: Design Automation Conf. (DAC), pp. 563–568. ACM, New York (2009) Google Scholar
  96. 96.
    Jain, H., Ivancic, F., Gupta, A., Shlyakhter, I., Wang, C.: Using statically computed invariants inside the predicate abstraction and refinement loop. In: Ball, T., Jones, R.B. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 4144, pp. 137–151. Springer, Heidelberg (2006) CrossRefGoogle Scholar
  97. 97.
    Järvisalo, M., Biere, A., Heule, M.: Simulating circuit-level simplifications on CNF. J. Autom. Reason. 49(4), 583–619 (2012) MathSciNetzbMATHCrossRefGoogle Scholar
  98. 98.
    Jhala, R., Majumdar, R.: Path slicing. In: Sarkar, V., Hall, M.W. (eds.) Conf. on Programming Language Design and Implementation (PLDI), pp. 38–47. ACM, New York (2005) Google Scholar
  99. 99.
    Jhala, R., Podelski, A., Rybalchenko, A.: Predicate abstraction for program verification. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018) Google Scholar
  100. 100.
    Jussila, T., Heljanko, K., Niemelä, I.: BMC via on-the-fly determinization. Electron. Notes Theor. Comput. Sci. 89(4), 561–577 (2003) zbMATHCrossRefGoogle Scholar
  101. 101.
    Kahlon, V., Wang, C., Gupta, A.: Monotonic partial order reduction: an optimal symbolic partial order reduction technique. In: Bouajjani, A., Maler, O. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 5643, pp. 398–413. Springer, Heidelberg (2009) CrossRefGoogle Scholar
  102. 102.
    Kaiser, A., Kroening, D., Wahl, T.: Dynamic cutoff detection in parameterized concurrent programs. In: Touili, T., Cook, B., Jackson, P. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 6174, pp. 654–659. Springer, Heidelberg (2010) Google Scholar
  103. 103.
    Kautz, H.A., Selman, B.: Pushing the envelope: planning, propositional logic and stochastic search. In: Clancey, W.J., Weld, D.S. (eds.) National Conf. on Artificial Intelligence (AAAI), pp. 1194–1201. AAAI Press/MIT Press, Portland/Cambridge (1996) Google Scholar
  104. 104.
    Khasidashvili, Z., Nadel, A.: Implicative simultaneous satisfiability and applications. In: Eder, K., Lourenço, J., Shehory, O. (eds.) Intl. Haifa Verification Conference (HVC). LNCS, vol. 7261, pp. 66–79. Springer, Heidelberg (2011) Google Scholar
  105. 105.
    King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385–394 (1976) MathSciNetzbMATHCrossRefGoogle Scholar
  106. 106.
    Kleine Büning, H., Bubeck, U.: Theory of quantified boolean formulas. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 735–760. IOS Press, Amsterdam (2009) Google Scholar
  107. 107.
    Kovásznai, G., Fröhlich, A., Biere, A.: On the complexity of fixed-size bit-vector logics with binary encoded bit-width. In: Fontaine, P., Goel, A. (eds.) Intl. Workshop on Satisfiability Modulo Theories (SMT), pp. 44–55 (2012). EasyChair Google Scholar
  108. 108.
    Kroening, D.: Application specific higher order logic theorem proving. In: Autexier, S., Mantel, H. (eds.) Proc. of the Verification Workshop (VERIFY), pp. 5–15 (2002) Google Scholar
  109. 109.
    Kroening, D.: Computing over-approximations with bounded model checking. Electron. Notes Theor. Comput. Sci. 144(1), 79–92 (2006) zbMATHCrossRefGoogle Scholar
  110. 110.
    Kroening, D.: Software verification. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 505–532. IOS Press, Amsterdam (2009) Google Scholar
  111. 111.
    Kroening, D., Clarke, E.: Checking consistency of C and Verilog using predicate abstraction and induction. In: Intl. Conf. on Computer-Aided Design (ICCAD), pp. 66–72. IEEE/ACM, Piscataway/New York (2004) Google Scholar
  112. 112.
    Kroening, D., Clarke, E., Yorav, K.: Behavioral consistency of C and Verilog programs using bounded model checking. In: Design Automation Conf. (DAC), pp. 368–371. ACM, New York (2003) Google Scholar
  113. 113.
    Kroening, D., Leroux, J., Rümmer, P.: Interpolating quantifier-free Presburger arithmetic. In: Fermüller, C.G., Voronkov, A. (eds.) Intl. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR). LNCS, vol. 6397, pp. 489–503. Springer, Heidelberg (2010) CrossRefGoogle Scholar
  114. 114.
    Kroening, D., Ouaknine, J., Seshia, S., Strichman, O.: Abstraction-based satisfiability solving of Presburger arithmetic. In: Alur, R., Peled, D.A. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 3114, pp. 308–320. Springer, Heidelberg (2004) CrossRefGoogle Scholar
  115. 115.
    Kroening, D., Ouaknine, J., Strichman, O., Wahl, T., Worrell, J.: Linear completeness thresholds for bounded model checking. In: Gopalakrishnan, G., Qadeer, S. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 6806, pp. 557–572. Springer, Heidelberg (2011) CrossRefGoogle Scholar
  116. 116.
    Kroening, D., Sharygina, N.: Approximating predicate images for bit-vector logic. In: Hermanns, H., Palsberg, J. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 3920, pp. 242–256. Springer, Heidelberg (2006) zbMATHGoogle Scholar
  117. 117.
    Kroening, D., Sharygina, N., Tonetta, S., Tsitovich, A., Wintersteiger, C.: Loopfrog: a static analyzer for ANSI-C programs. In: Intl. Conf. on Automated Software Engineering (ASE), pp. 668–670. IEEE, Piscataway (2009) Google Scholar
  118. 118.
    Kroening, D., Sharygina, N., Tonetta, S., Tsitovich, A., Wintersteiger, C.M.: Loop summarization using abstract transformers. In: Cha, S.D., Choi, J., Kim, M., Lee, I., Viswanathan, M. (eds.) Intl. Symp. on Automated Technology for Verification and Analysis (ATVA). LNCS, vol. 5311, pp. 111–125. Springer, Heidelberg (2008) CrossRefGoogle Scholar
  119. 119.
    Kroening, D., Strichman, O.: Efficient computation of recurrence diameters. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI). LNCS, vol. 2575, pp. 298–309. Springer, Heidelberg (2003) CrossRefGoogle Scholar
  120. 120.
    Kroening, D., Strichman, O.: Decision Procedures. Springer, Heidelberg (2008) zbMATHGoogle Scholar
  121. 121.
    Kroening, D., Weissenbacher, G.: Counterexamples with loops for predicate abstraction. In: Ball, T., Jones, R.B. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 4144, pp. 152–165. Springer, Heidelberg (2006) CrossRefGoogle Scholar
  122. 122.
    Kuehlmann, A.: Dynamic transition relation simplification for bounded property checking. In: Intl. Conf. on Computer-Aided Design (ICCAD), pp. 50–57. IEEE/ACM, Piscataway/New York (2004) Google Scholar
  123. 123.
    Kuehlmann, A., Paruthi, V., Krohm, F., Ganai, M.K.: Robust boolean reasoning for equivalence checking and functional property verification. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. 21(12), 1377–1394 (2002) CrossRefGoogle Scholar
  124. 124.
    Kuismin, T., Heljanko, K.: Increasing confidence in liveness model checking results with proofs. In: Bertacco, V., Legay, A. (eds.) Intl. Haifa Verification Conference (HVC). LNCS, vol. 8244, pp. 32–43. Springer, Heidelberg (2013) Google Scholar
  125. 125.
    Kurshan, R.P.: Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, Princeton (1994) zbMATHGoogle Scholar
  126. 126.
    Lahiri, S.K., Qadeer, S., Rakamaric, Z.: Static and precise detection of concurrency errors in systems code using SMT solvers. In: Bouajjani, A., Maler, O. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 5643, pp. 509–524. Springer, Heidelberg (2009) CrossRefGoogle Scholar
  127. 127.
    Lal, A., Reps, T.W.: Reducing concurrent analysis under a context bound to sequential analysis. Form. Methods Syst. Des. 35(1), 73–97 (2009) zbMATHCrossRefGoogle Scholar
  128. 128.
    Latvala, T., Biere, A., Heljanko, K., Junttila, T.A.: Simple bounded LTL model checking. In: Hu, A.J., Martin, A.K. (eds.) Formal Methods in Computer Aided Design (FMCAD). LNCS, vol. 3312, pp. 186–200. Springer, Heidelberg (2004) CrossRefGoogle Scholar
  129. 129.
    Li, B., Somenzi, F.: Efficient abstraction refinement in interpolation-based unbounded model checking. In: Hermanns, H., Palsberg, J. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 3920, pp. 227–241. Springer, Heidelberg (2006) Google Scholar
  130. 130.
    Li, B., Wang, C., Somenzi, F.: Abstraction refinement in symbolic model checking using satisfiability as the only decision procedure. Softw. Tools Technol. Transf. 7(2), 143–155 (2005) CrossRefGoogle Scholar
  131. 131.
    McMillan, K.L.: Applying SAT methods in unbounded symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 2404, pp. 250–264. Springer, Heidelberg (2002) CrossRefGoogle Scholar
  132. 132.
    McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt, W.A. Jr., Somenzi, F. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003) CrossRefGoogle Scholar
  133. 133.
    McMillan, K.L.: An interpolating theorem prover. In: Jensen, K., Podelski, A. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 2988, pp. 16–30. Springer, Heidelberg (2004) Google Scholar
  134. 134.
    McMillan, K.L.: Interpolation and model checking. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018) Google Scholar
  135. 135.
    McMillan, K.L., Amla, N.: Automatic abstraction without counterexamples. In: Garavel, H., Hatcliff, J. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 2619, pp. 2–17. Springer, Heidelberg (2003) Google Scholar
  136. 136.
    Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Design Automation Conf. (DAC), pp. 530–535. ACM, New York (2001) Google Scholar
  137. 137.
    de Moura, L.M., Bjørner, N.: Generalized, efficient array decision procedures. In: Formal Methods in Computer Aided Design (FMCAD), pp. 45–52. IEEE, Piscataway (2009) Google Scholar
  138. 138.
    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) MathSciNetzbMATHCrossRefGoogle Scholar
  139. 139.
    Penczek, W., Wozna, B., Zbrzezny, A.: Bounded model checking for the universal fragment of CTL. Fundam. Inform. 51(1–2), 135–156 (2002) MathSciNetzbMATHGoogle Scholar
  140. 140.
    Piterman, N., Pnueli, A.: Temporal logic and fair discrete systems. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018) Google Scholar
  141. 141.
    Prasad, M., Biere, A., Gupta, A.: A survey on recent advances in SAT-based formal verification. Softw. Tools Technol. Transf. 7(2), 156–173 (2005) CrossRefGoogle Scholar
  142. 142.
    Prestwich, S.D.: CNF encodings. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 75–97. IOS Press, Amsterdam (2009) Google Scholar
  143. 143.
    Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, L.D. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 3440, pp. 93–107. Springer, Heidelberg (2005) zbMATHGoogle Scholar
  144. 144.
    Rabinovitz, I., Grumberg, O.: Bounded model checking of concurrent programs. In: Etessami, K., Rajamani, S.K. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 3576, pp. 82–97. Springer, Heidelberg (2005) CrossRefGoogle Scholar
  145. 145.
    Rintanen, J.: Planning as satisfiability: heuristics. Artif. Intell. 193, 45–86 (2012) MathSciNetzbMATHCrossRefGoogle Scholar
  146. 146.
    Schuppan, V., Biere, A.: Efficient reduction of finite state model checking to reachability analysis. Softw. Tools Technol. Transf. 5(1–2), 185–204 (2004) CrossRefGoogle Scholar
  147. 147.
    Sebastiani, R.: Lazy satisfiability modulo theories. J. Satisf. Boolean Model. Comput. 3(3–4), 141–224 (2007) MathSciNetzbMATHGoogle Scholar
  148. 148.
    Sheeran, M., Singh, S., Stålmarck, G.: Checking safety properties using induction and a SAT-solver. In: Hunt, W.A. Jr., Johnson, S.D. (eds.) Formal Methods in Computer Aided Design (FMCAD). LNCS, vol. 1954, pp. 108–125. Springer, Heidelberg (2000) Google Scholar
  149. 149.
    Sinha, N., Wang, C.: Staged concurrent program analysis. In: Roman, G.C., Sullivan, K.J. (eds.) Intl. Symp. on Foundations of Software Engineering (FSE), pp. 47–56. ACM, New York (2010) Google Scholar
  150. 150.
    Sinha, N., Wang, C.: On interference abstractions. In: Ball, T., Sagiv, M. (eds.) Symp. on Principles of Programming Languages (POPL), pp. 423–434. ACM, New York (2011) Google Scholar
  151. 151.
    Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Studies in Constructive Mathematics and Mathematical Logic, Part II. Seminars in Mathematics, vol. 8, pp. 234–259 (1968). V.A. Steklov Mathematical Institute. English Translation, Consultants Bureau, pp. 115–125 (1970) Google Scholar
  152. 152.
    Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1–37 (1994) MathSciNetzbMATHCrossRefGoogle Scholar
  153. 153.
    Velev, M.N.: Efficient translation of boolean formulas to CNF in formal verification of microprocessors. In: Imai, M. (ed.) Asia and South Pacific Design Automation Conf. (ASPDAC), pp. 310–315. IEEE, Piscataway (2004) Google Scholar
  154. 154.
    Vijayaraghavan, S., Ramanathan, M.: A Practical Guide for SystemVerilog Assertions. Springer, Heidelberg (2005) Google Scholar
  155. 155.
    Vizel, Y., Weissenbacher, G., Malik, S.: Boolean satisfiability solvers and their applications in model checking. Proc. IEEE 103(11), 2021–2035 (2015). doi: 10.1109/JPROC.2015.2455034 CrossRefGoogle Scholar
  156. 156.
    Weissenbacher, G., Kroening, D.: An interpolating decision procedure for transitive relations with uninterpreted functions. In: Namjoshi, K.S., Zeller, A., Ziv, A. (eds.) Intl. Haifa Verification Conference (HVC). LNCS, vol. 6405, pp. 150–168. Springer, Heidelberg (2009) Google Scholar
  157. 157.
    Witkowski, T., Blanc, N., Weissenbacher, G., Kroening, D.: Model checking concurrent Linux device drivers. In: Stirewalt, R.E.K., Egyed, A., Fischer, B. (eds.) Intl. Conf. on Automated Software Engineering (ASE), pp. 501–504. ACM, New York (2007) Google Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  1. 1.Johannes Kepler UniversityLinzAustria
  2. 2.University of OxfordOxfordUK

Personalised recommendations