Advertisement

Pruning Techniques for the SAT-Based Bounded Model Checking Problem

  • Ofer Shtrichman
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2144)

Abstract

Bounded Model Checking (BMC) is the problem of checking if a model satisfies a temporal property in paths with bounded length k. Propositional SAT-based BMC is conducted in a gradual manner, by solving a series of SAT instances corresponding to formulations of the problem with increasing k. We show how the gradual nature can be exploited for shortening the overall verification time. The concept is to reuse constraints on the search space which are deduced while checking a k instance, for speeding up the SAT checking of the consecutive k+1 instance. This technique can be seen as a generalization of‘pervasive clauses’, a technique introduced by Silva and Sakallah in the context of Automatic Test Pattern Generation (ATPG). We define the general conditions for reusability of constraints, and define a simple procedure for evaluating them. This technique can theoretically be used in any solution that is based on solving a series of closely related SAT instances (instances with non-empty intersection between their set of clauses). We then continue by showing how a similar procedure can be used for restricting the search space of individual SAT instances corresponding to BMC invariant formulas. Experiments demonstrated that both techniques have consistent and significant positive effect.

Keywords

Satisfying Assignment Bounded Model Check Automatic Test Pattern Generation Constraint Sharing Current Partial Assignment 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Proceedings of the Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS99), Lect. Notes in Comp. Sci. Springer-Verlag, 1999.Google Scholar
  2. 2.
    A. Biere, E. Clarke, R. Raimi, and Y. Zhu. Verifying safety properties of a power pc TM microprocessor using symbolic model checking without bdds. In N. Halbwachs and D. Peled, editors, Proc. 11 th Intl. Conference on Computer Aided Verification (CAV’99), Lect. Notes in Comp. Sci. Springer-Verlag, 1999.Google Scholar
  3. 3.
    R. I. Brafman and H. H. Hoos. To encode or not to encode: linear planning. IJCAI, pages 988–993, 1999.Google Scholar
  4. 4.
    M. Davis and H. Putnam. A computing procedure for quantification theory. J. ACM, 7:201–215, 1960.zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    L.G.e. Silva, L.M. Silveira, and J.P.M. Silva. Algorithms for solving boolean satisfiability in combinational circuits. In Proceedings of the IEEE/ACM Design, Automation and Test in Europe Conference (DATE), March 1999.Google Scholar
  6. 6.
    J.F. Groote, J.W.C. Koorn, and S.F.M. van Vlijmen. The safety guaranteeing system at station Hoorn-Kersenboogerd. Logic Group Preprint Series 121, Utrecht University, 1994.Google Scholar
  7. 7.
    J. N. Hooker. Solving the incremental satisfiability problem. Journal of Logic Programming, 15:177–186, 1993.zbMATHCrossRefMathSciNetGoogle Scholar
  8. 8.
    J.P.M. Silva and K. A. Sakallah. Robust search algorithms for test pattern generation. In Proceedings of the IEEE Fault-Tolerant Computing Symposium, June 1997.Google Scholar
  9. 9.
    H. Kautz and B. Selman. Planning as satisfiability. In Proc. of the 10th European Conf. on AI, pages 359–363, 1992.Google Scholar
  10. 10.
    J. Kim, J. Whittemore, J.P.M. Silva, and K. A. Sakallah. Incremental boolean satisfiability and its application to delay fault testing. In IEEE/ACM International Workshop on Logic Synthesis (IWLS), June 1999.Google Scholar
  11. 11.
    M. Sheeran, S. Singh, and G. Stalmarck. Checking safety properties using induction and a sat-solver. In Hunt and Johnson, editors, Proc. Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD 2000), 2000.Google Scholar
  12. 12.
    O. Shtrichman. Tuning SAT checkers for bounded model checking. In E.A. Emerson and A.P. Sistla, editors, Proc. 12 th Intl. Conference on Computer Aided Verification (CAV’00), Lect. Notes in Comp. Sci. Springer-Verlag, 2000.Google Scholar
  13. 13.
    J.P.M. Silva and K. A. Sakallah. GRASP-a new search algorithm for satisfiability. Technical Report TR-CSE-292996, Univerisity of Michigen, 1996.Google Scholar
  14. 14.
    J.P.M. Silva and K. A. Sakallah. GRASP: A search algorithm for propositional satisfiability. IEEE Transactions on Computers, 48:506–516, 1999.CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Ofer Shtrichman
    • 1
    • 2
  1. 1.The Minerva Center for Verification of Reactive Systems, at the Dep. of Computer Science and Applied MathematicsThe Weizmann Institute of ScienceIsrael
  2. 2.IBM Haifa Research LabUSA

Personalised recommendations