×

zbMATH — the first resource for mathematics

SAT-based model checking. (English) Zbl 1392.68232
Clarke, Edmund M. (ed.) et al., Handbook of model checking. Cham: Springer (ISBN 978-3-319-10574-1/hbk; 978-3-319-10575-8/ebook). 277-303 (2018).
Summary: 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.
For the entire collection see [Zbl 1390.68001].

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDF BibTeX XML Cite
Full Text: DOI
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) · Zbl 0971.68633
[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)
[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)
[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) · Zbl 1117.68420
[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) · Zbl 1103.68603
[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)
[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) · Zbl 1272.68221
[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)
[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)
[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) · Zbl 1103.68604
[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) · Zbl 0978.68540
[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) · Zbl 0976.68540
[13] 13. Ball, T., Rajamani, S.K.: Boolean programs: a model and process for software analysis. Tech. rep., Microsoft Research (2000) · Zbl 0976.68540
[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)
[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)
[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) · Zbl 1392.68379
[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)
[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) · Zbl 1242.68055
[19] 19. Basler, G., Mazzucchi, M., Wahl, T., Kroening, D.: Context-aware counter abstraction. Form. Methods Syst. Des. 36(3), 223-245 (2010) · Zbl 1213.68362
[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)
[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) · Zbl 1010.68514
[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) · Zbl 1132.68333
[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)
[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)
[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)
[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)
[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) · Zbl 1127.68057
[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) · Zbl 1183.68568
[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)
[30] 30. Blanc, N., Kroening, D.: Race analysis for SystemC using model checking. ACM Trans. Des. Autom. Electron. Syst. 15(3), 1-32 (2010)
[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)
[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)
[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) · Zbl 1317.68109
[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) · Zbl 1273.68222
[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)
[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) · Zbl 1291.03112
[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) · Zbl 1318.03045
[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)
[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)
[40] 40. Bryant, R.E.: Graph Based Algorithms for Boolean Function Manipulation. Trans. Comput. C-35(8), 677-691 (1986) · Zbl 0593.94022
[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) · Zbl 1186.68281
[42] 42. Büchi, J.R.: Regular canonical systems. Arch. Math. Log. 6(3-4), 91-111 (1964)
[43] 43. Cadar, C., Sen, K.: Symbolic execution for software testing: Three decades later. Commun. ACM 56(2), 82-90 (2013)
[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)
[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)
[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)
[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)
[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)
[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)
[50] 50. Clarke, E., Jain, H., Kroening, D.: Verification of SpecC using predicate abstraction. Form. Methods Syst. Des. 30(1), 5-28 (2007) · Zbl 1117.68046
[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)
[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) · Zbl 1126.68470
[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) · Zbl 1090.68022
[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) · Zbl 1087.68586
[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) · Zbl 1325.68145
[56] 56. Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. Trans. Program. Lang. Syst. 16(5), 1512-1542 (1994)
[57] 57. Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999) · Zbl 1423.68002
[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)
[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) · Zbl 1081.68673
[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)
[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) · Zbl 1290.68112
[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)
[63] 63. Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. Tech. rep., HP Labs (2003) · Zbl 1323.68462
[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) · Zbl 1317.68113
[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)
[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)
[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) · Zbl 1301.68156
[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) · Zbl 1352.68060
[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)
[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) · Zbl 1243.68213
[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)
[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) · Zbl 1214.68351
[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)
[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)
[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)
[76] 76. Eisner, C., Fisman, D.: A Practical Introduction to PSL. Springer, Heidelberg (2006)
[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) · Zbl 1392.68247
[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) · Zbl 1284.68087
[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) · Zbl 0907.68126
[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)
[81] 81. Ganai, M.K., Gupta, A.: SAT-Based Scalable Formal Verification Solutions. Springer, Heidelberg (2007) · Zbl 1138.68037
[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)
[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)
[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)
[85] 85. Groce, A., Kroening, D.: Making the most of BMC counterexamples. Electron. Notes Theor. Comput. Sci. 119, 67-81 (2005) · Zbl 1272.68252
[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)
[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) · Zbl 1103.68620
[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) · Zbl 1392.68251
[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)
[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) · Zbl 1188.68189
[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) · Zbl 1081.68621
[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) · Zbl 1325.68147
[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) · Zbl 1273.68229
[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)
[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)
[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)
[97] 97. Järvisalo, M., Biere, A., Heule, M.: Simulating circuit-level simplifications on CNF. J. Autom. Reason. 49(4), 583-619 (2012) · Zbl 1267.94144
[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)
[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) · Zbl 1392.68253
[100] 100. Jussila, T., Heljanko, K., Niemelä, I.: BMC via on-the-fly determinization. Electron. Notes Theor. Comput. Sci. 89(4), 561-577 (2003) · Zbl 1271.68138
[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) · Zbl 1242.68166
[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)
[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)
[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)
[105] 105. King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385-394 (1976) · Zbl 0329.68018
[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)
[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
[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)
[109] 109. Kroening, D.: Computing over-approximations with bounded model checking. Electron. Notes Theor. Comput. Sci. 144(1), 79-92 (2006) · Zbl 1272.68264
[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)
[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)
[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)
[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) · Zbl 1306.68148
[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) · Zbl 1103.68626
[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) · Zbl 1360.68592
[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) · Zbl 1180.68175
[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)
[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) · Zbl 1183.68377
[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) · Zbl 1022.68579
[120] 120. Kroening, D., Strichman, O.: Decision Procedures. Springer, Heidelberg (2008) · Zbl 1149.68071
[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)
[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)
[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)
[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)
[125] 125. Kurshan, R.P.: Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, Princeton (1994) · Zbl 0822.68116
[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)
[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) · Zbl 1186.68298
[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) · Zbl 1117.68432
[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) · Zbl 1180.68176
[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)
[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) · Zbl 1010.68509
[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) · Zbl 1278.68184
[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) · Zbl 1126.68573
[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) · Zbl 1392.68260
[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) · Zbl 1031.68520
[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)
[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)
[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) · Zbl 1326.68164
[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) · Zbl 1052.68087
[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) · Zbl 1392.68263
[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)
[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)
[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) · Zbl 1087.68598
[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) · Zbl 1081.68633
[145] 145. Rintanen, J.: Planning as satisfiability: heuristics. Artif. Intell. 193, 45-86 (2012) · Zbl 1270.68276
[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)
[147] 147. Sebastiani, R.: Lazy satisfiability modulo theories. J. Satisf. Boolean Model. Comput. 3(3-4), 141-224 (2007) · Zbl 1145.68501
[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)
[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)
[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) · Zbl 1284.68203
[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) · Zbl 0197.00102
[152] 152. Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1-37 (1994) · Zbl 0827.03009
[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)
[154] 154. Vijayaraghavan, S., Ramanathan, M.: A Practical Guide for SystemVerilog Assertions. Springer, Heidelberg (2005)
[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:
[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)
[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)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.