Model checking with Boolean Satisfiability

L. Baptista, J.P. Marques-Silva, Using randomization and learning to solve hard real-world instances of satisfiability, in: International Conference on Principles and Practice of Constraint Programming, September 2000, pp. 489–494 Beame, 2004, Towards understanding and harnessing the potential of clause learning, J. Artificial Intelligence Res., 22, 319, 10.1613/jair.1410 Biere Biere, 2003 A. Biere, A. Cimatti, E. Clarke, Y. Zhu, Symbolic model checking without BDDs, in: Tools and Algorithms for the Construction and Analysis of Systems, March 1999, pp. 193–207 P. Bjesse, K. Claesen, SAT-based verification without state space traversal, in: Formal Methods in Computer-Aided Design, 2000, pp. 372–389 G. Cabodi, M. Murciano, S. Nocco, S. Quer, Stepping forward with interpolants in unbounded model checking, in: International Conference on Computer-Aided Design, 2006, pp. 772–778 P. Chauhan, E. Clarke, J. Kukula, S. Sapra, H. Veith, D. Wang, Automated abstraction refinement for model checking large state spaces using SAT based conflict analysis, in: Formal Methods in Computer-Aided Design, 2002, pp. 33–51 Clarke, 1999 F. Copty, L. Fix, R. Fraer, E. Giunchiglia, G. Kamhi, A. Tacchella, M.Y. Vardi, Benefits of bounded model checking at an industrial setting, in: Computer-Aided Verification, 2001, pp. 436–453 Craig, 1957, Linear reasoning: A new form of the Herbrand–Gentzen theorem, J. Symbolic Logic, 22, 250, 10.2307/2963593 Davis, 1962, A machine program for theorem-proving, Comm. of the ACM, 5, 394, 10.1145/368273.368557 Davis, 1960, A computing procedure for quantification theory, J. ACM, 7, 201, 10.1145/321033.321034 N. Een, N. Sörensson, An extensible SAT solver, in: International Conference on Theory and Applications of Satisfiability Testing, May 2003, pp. 502–518 Een, 2003, Temporal induction by incremental SAT solving, vol. 89 M. Glusman, G. Kamhi, S. Mador-Haim, R. Fraer, M. Vardi, Multiple-counterexample guided iterative abstraction refinement, in: Tools and Algorithms for the Construction and Analysis of Systems, April 2003, pp. 176–191 E. Goldberg, Y. Novikov, BerkMin: A fast and robust SAT-solver, in: Design, Automation and Testing in Europe Conference, March 2002, pp. 142–149 C.P. Gomes, B. Selman, H. Kautz, Boosting combinatorial search through randomization, in: AAAI Conference on Artificial Intelligence, July 1998, pp. 431–437 A. Gupta, M. Ganai, Z. Yang, P. Ashar, Iterative abstraction using SAT-based BMC with proof analysis, in: International Conference on Computer-Aided Design, November 2003, pp. 416–423 Huth, 2004 H.-J. Kang, I.-C. Park, SAT-based unbounded symbolic model checking, in: Design Automation Conference, June 2003, pp. 840–843 Krajicek, 1997, Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic, J. Symbolic Logic, 62, 457, 10.2307/2275541 J. Marques-Silva, Improvements to the implementation of interpolant-based model checking, in: Advanced Research Working Conference on Correct Hardware Design and Verification Methods, October 2005, pp. 367–370 J. Marques-Silva, Interpolant learning and reuse in SAT-based model checking, in: Electron. Notes Theor. Comput. Sci., vol. 174(3), Elsevier, 2007, pp. 31–43 J. Marques-Silva, K. Sakallah, GRASP: A new search algorithm for satisfiability, in: International Conference on Computer-Aided Design, November 1996, pp. 220–227 Marques-Silva, 1999, GRASP—A search algorithm for propositional satisfiability, IEEE Trans. Comput., 48, 506, 10.1109/12.769433 McMillan, 1993 K.L. McMillan, Applying SAT methods in unbounded symbolic model checking, in: Computer-Aided Verification, July 2002, pp. 250–264 K.L. McMillan, Interpolation and SAT-based model checking, in: Computer-Aided Verification, 2003, pp. 1–13 K.L. McMillan, N. Amla, Automatic abstraction without counterexamples, in: Tools and Algorithms for the Construction and Analysis of Systems, April 2003, pp. 2–17 M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, S. Malik, Engineering an efficient SAT solver, in: Design Automation Conference, June 2001, pp. 530–535 Plaisted, 1986, A structure-preserving clause form translation, J. Symbolic Comput., 2, 293, 10.1016/S0747-7171(86)80028-1 Pudlák, 1997, Lower bounds for resolution and cutting planes proofs and monotone circuit computations, J. Symbolic Logic, 62, 981, 10.2307/2275583 M. Sheeran, S. Singh, G. Stalmarck, Checking safety properties using induction and a SAT solver, in: Formal Methods in Computer-Aided Design, 2000, pp. 108–125 O. Strichman, Tuning SAT checkers for bounded model checking, in: Computer-Aided Verification, July 2000, pp. 480–494 G.S. Tseitin, On the complexity of derivation in propositional calculus, in: Studies in Constructive Mathematics and Mathematical Logic, Part II, 1968, pp. 115–125 R. Zabih, D.A. McAllester, A rearrangement search strategy for determining propositional satisfiability, in: AAAI Conference on Artificial Intelligence, July 1988, pp. 155–160 L. Zhang and S. Malik, Validating SAT solvers using an independent resolution-based checker: Practical implementations and other applications, in: Design, Automation and Testing in Europe Conference, March 2003, pp. 10880–10885