Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

SAT-Based Model Checking

  • Chapter
  • First Online:
Handbook of Model Checking

  • 11k Accesses

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  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)

    MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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. 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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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. Awedh, M., Somenzi, F.: Termination criteria for bounded model checking: extensions and comparison. Electron. Notes Theor. Comput. Sci. 144(1), 51–66 (2006)

    Article  MATH  Google Scholar 

  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. 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. 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)

    Chapter  Google Scholar 

  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. 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)

    Chapter  Google Scholar 

  13. Ball, T., Rajamani, S.K.: Boolean programs: a model and process for software analysis. Tech. rep., Microsoft Research (2000)

    Google Scholar 

  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. 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. 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. 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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  19. Basler, G., Mazzucchi, M., Wahl, T., Kroening, D.: Context-aware counter abstraction. Form. Methods Syst. Des. 36(3), 223–245 (2010)

    Article  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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. 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. 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. 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. 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)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    MATH  Google Scholar 

  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. Blanc, N., Kroening, D.: Race analysis for SystemC using model checking. ACM Trans. Des. Autom. Electron. Syst. 15(3), 1–32 (2010)

    Article  Google Scholar 

  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. 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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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. 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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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. 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. Bryant, R.E.: Graph Based Algorithms for Boolean Function Manipulation. Trans. Comput. C-35(8), 677–691 (1986)

    Article  MATH  Google Scholar 

  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. Büchi, J.R.: Regular canonical systems. Arch. Math. Log. 6(3–4), 91–111 (1964)

    MathSciNet  MATH  Google Scholar 

  43. Cadar, C., Sen, K.: Symbolic execution for software testing: Three decades later. Commun. ACM 56(2), 82–90 (2013)

    Article  Google Scholar 

  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. 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. 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. 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)

    Article  Google Scholar 

  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)

    Chapter  Google Scholar 

  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. Clarke, E., Jain, H., Kroening, D.: Verification of SpecC using predicate abstraction. Form. Methods Syst. Des. 30(1), 5–28 (2007)

    Article  MATH  Google Scholar 

  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. 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. 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)

    Article  MATH  Google Scholar 

  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)

    MATH  Google Scholar 

  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)

    Article  MathSciNet  MATH  Google Scholar 

  56. Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. Trans. Program. Lang. Syst. 16(5), 1512–1542 (1994)

    Article  Google Scholar 

  57. Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)

    Google Scholar 

  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)

    Article  Google Scholar 

  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)

    Chapter  MATH  Google Scholar 

  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. 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)

    Chapter  Google Scholar 

  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. Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. Tech. rep., HP Labs (2003)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  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. 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)

    Chapter  Google Scholar 

  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. 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)

    MATH  Google Scholar 

  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)

    Article  Google Scholar 

  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)

    Article  MATH  Google Scholar 

  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. 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)

    MATH  Google Scholar 

  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)

    Chapter  MATH  Google Scholar 

  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. 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)

    Article  Google Scholar 

  76. Eisner, C., Fisman, D.: A Practical Introduction to PSL. Springer, Heidelberg (2006)

    Google Scholar 

  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)

    MATH  Google Scholar 

  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. Finkel, A., Willems, B., Wolper, P.: A direct symbolic approach to model checking pushdown systems. Electron. Notes Theor. Comput. Sci. 9, 27–37 (1997)

    Article  MATH  Google Scholar 

  80. Gan, X., Dubrovin, J., Heljanko, K.: A symbolic model checking approach to verifying satellite onboard software. Sci. Comput. Program. 82, 44–55 (2014)

    Article  Google Scholar 

  81. Ganai, M.K., Gupta, A.: SAT-Based Scalable Formal Verification Solutions. Springer, Heidelberg (2007)

    Book  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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. 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)

    Chapter  Google Scholar 

  85. Groce, A., Kroening, D.: Making the most of BMC counterexamples. Electron. Notes Theor. Comput. Sci. 119, 67–81 (2005)

    Article  MATH  Google Scholar 

  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. 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)

    Chapter  Google Scholar 

  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)

    MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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. 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. 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. 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. 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)

    Chapter  Google Scholar 

  97. Järvisalo, M., Biere, A., Heule, M.: Simulating circuit-level simplifications on CNF. J. Autom. Reason. 49(4), 583–619 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  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. 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. Jussila, T., Heljanko, K., Niemelä, I.: BMC via on-the-fly determinization. Electron. Notes Theor. Comput. Sci. 89(4), 561–577 (2003)

    Article  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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. 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. 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. King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385–394 (1976)

    Article  MathSciNet  MATH  Google Scholar 

  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. 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. 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. Kroening, D.: Computing over-approximations with bounded model checking. Electron. Notes Theor. Comput. Sci. 144(1), 79–92 (2006)

    Article  MATH  Google Scholar 

  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. 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. 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. 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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    MATH  Google Scholar 

  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. 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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  120. Kroening, D., Strichman, O.: Decision Procedures. Springer, Heidelberg (2008)

    MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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. 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)

    Article  Google Scholar 

  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. Kurshan, R.P.: Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, Princeton (1994)

    MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Article  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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. 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)

    Article  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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. 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. 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. 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. 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. 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)

    Article  MathSciNet  MATH  Google Scholar 

  139. Penczek, W., Wozna, B., Zbrzezny, A.: Bounded model checking for the universal fragment of CTL. Fundam. Inform. 51(1–2), 135–156 (2002)

    MathSciNet  MATH  Google Scholar 

  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. 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)

    Article  Google Scholar 

  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. 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)

    MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  145. Rintanen, J.: Planning as satisfiability: heuristics. Artif. Intell. 193, 45–86 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Article  Google Scholar 

  147. Sebastiani, R.: Lazy satisfiability modulo theories. J. Satisf. Boolean Model. Comput. 3(3–4), 141–224 (2007)

    MathSciNet  MATH  Google Scholar 

  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. 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. 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. 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. Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1–37 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  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. Vijayaraghavan, S., Ramanathan, M.: A Practical Guide for SystemVerilog Assertions. Springer, Heidelberg (2005)

    Google Scholar 

  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

    Article  Google Scholar 

  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. 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 

Download references

Author information

Authors and Affiliations

  1. Johannes Kepler University, Linz, Austria

    Armin Biere

  2. University of Oxford, Oxford, UK

    Daniel Kröning

Authors
  1. Armin Biere
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Daniel Kröning
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Armin Biere .

Editor information

Editors and Affiliations

  1. FORE Systems University Professor of Computer Science, Carnegie Mellon University, Pittsburgh, Pennsylvania, USA

    Edmund M. Clarke

  2. Institute of Science and Technology Austria (IST), Klosterneuburg, Austria

    Thomas A. Henzinger

  3. Arbeitsbereich Formal Methods in Systems Engineering, Technische Universität Wien, Wien, Austria

    Helmut Veith

  4. Institut f. Angewandte Informationsverarbeitung und Kommunikationstechnologie (IAIK), Technische Universität Graz, Graz, Austria

    Roderick Bloem

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Biere, A., Kröning, D. (2018). SAT-Based Model Checking. In: Clarke, E., Henzinger, T., Veith, H., Bloem, R. (eds) Handbook of Model Checking. Springer, Cham. https://doi.org/10.1007/978-3-319-10575-8_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-10575-8_10

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-10574-1

  • Online ISBN: 978-3-319-10575-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation