Advertisement

SAT-Based Verification without State Space Traversal

  • Per Bjesse
  • Koen Claessen
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1954)

Abstract

Binary Decision Diagrams (BDDs) have dominated the area of symbolic model checking for the past decade. Recently, the use of satisfiability (SAT) solvers has emerged as an interesting complement to BDDs. SAT-based methods are capable of coping with some of the systems that BDDs are unable to handle. The most challenging problem that has to be solved in order to adapt standard symbolic model checking to SAT-solvers is the boolean quanti fication necessary for traversing the state space. A possible approach to extending the applicability of SAT-based model checkers is therefore to reduce the amount of traversal. In this paper, we investigate a BDD-based verification algorithm due to van Eijk. Van Eijk’s algorithm tries to compute information that is sufficient to prove a given safety property directly. When this is not possible, the computed information can be used to reduce the amount of traversal needed by standard model checking algorithms. We convert van Eijk’s algorithm to use a SAT-solver instead of BDDs. We also make a number of improvements to the original algorithm, such as combining it with recently developed variants of induction. The result is a collection of substantially strengthened and complete verification methods that do not require state space traversal.

Keywords

Model Check Safety Property Reachable State Binary Decision Diagram Reachability Analysis 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    P. A. Abdulla, P. Bjesse, and N. Eén. Symbolic reachability analysis based on SAT-solvers. In Proc. TACAS ’00, 9 th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, 2000.Google Scholar
  2. 2.
    A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Proc. TACAS’ 99, 8 th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, 1999.Google Scholar
  3. 3.
    R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Trans. on Computers, C-35(8):677–691, Aug. 1986.CrossRefGoogle Scholar
  4. 4.
    E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, December 1999.Google Scholar
  5. 5.
    P. Cousot and R. Cousot. Abstract interpretation: A unified model for static analysis of programs by construction or approximation of fixpoints. In Proc. 4 th ACM Symp. on Principles of Programming Languages, pages 238–252, 1977.Google Scholar
  6. 6.
    C. A. J. van Eijk. Sequential equivalence checking without state space traversal. In Proc. Conf. on Design, Automation and Test in Europe, 1998.Google Scholar
  7. 7.
    S. G. Govindaraju and D. L. Dill. Approximate symbolic model checking using overlapping projections. In Electronic Notes in Theoretical Computer Science, July 1999. Trento, Italy.Google Scholar
  8. 8.
    N. Halbwachs. About synchronous programming and abstract interpretation. In B. LeCharlier, editor, International Symposium on Static Analysis, SAS’94, Namur, Belgium, September 1994. LNCS 864, Springer Verlag.Google Scholar
  9. 9.
    N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. The synchronous dataflow programming language Lustre. Proceedings of the IEEE, 79(9):1305–1320, September 1991.Google Scholar
  10. 10.
    N. Halbwachs, Y. E. Proy, and P. Roumanoff. Verification of real-time systems using linear relation analysis. Formal Methods in System Design, 11(2):157–185, August 1997.CrossRefGoogle Scholar
  11. 11.
    Z. Manna and the STeP group. STeP: The Stanford Temporal Prover. Technical report, Computer Science Department, Stanford University, July 1994.Google Scholar
  12. 12.
    M. Sheeran, S. Singh, and G. Stålmarck. Checking safety properties using induction and a SAT-solver. In Formal Methods in Computer Aided Design, 2000.Google Scholar
  13. 13.
    M. Sheeran and G. Stålmarck. A tutorial on Stålmarck’s method of propositional proof. Formal Methods In System Design, 16(1), 2000.Google Scholar
  14. 14.
    G. Stålmarck. A system for determining propositional logic theorems by applying values and rules to triplets that are generated from a formula. Swedish Patent No. 467076 (1992), U.S. Patent No. 5 276 897 (1994), European Patent No. 0403 454 (1995), 1989.Google Scholar
  15. 15.
    P. F. Williams, A. Biere, E. M. Clarke, and A. Gupta. Combining decision diagrams and SAT procedures for efficient symbolic model checking. In Proc. 12 th Int. Conf. on Computer Aided Verification, 2000.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Per Bjesse
    • 1
  • Koen Claessen
    • 1
  1. 1.Department of Computing ScienceChalmers University of TechnologyGöteborg

Personalised recommendations