SAT-Based Model Checking
Much of the success of symbolic model checking is due to the use of Binary Decision Diagrams (BDDs) . which are canonical data structures for representing and manipulating formulas. Recently several works have suggested the use of propositional satisfiability solvers (SAT-solvers ). as an alternative to BDDs in symbolic model checking. The main motivation for these works is that both theoretical and practical evidence exist that the performances of SAT-solvers and BDDs vary in different applications. One important objective of this project is to evaluate our efforts on end-user applications provided by our industrial partner Prover Technology.
Contributions
- Reachability Analysis of Finite-State Systems [ABE00]
We show how to adapt standard algorithms for symbolic reachability analysis to work with SAT-solvers. The key element of our contribution is the combination of an algorithm that removes quantifiers over propositional variables and a simple representation that allows reuse of subformulas. The result will in principle allow many existing BDD-based algorithms to work with SAT-solvers. We show that even with our relatively simple techniques it is possible to verify systems that are known to be hard for BDD-based model checkers. The work is a cooperation with Per Bjesse and Niklas Eén at Department of Computer Science, Chalmers University of Technology.
- SAT-based Analysis of Unbounded Petri Nets. [AIN01]
We show how to use a SAT-solver to analyze the coverability problem for unbounded Petri nets. The idea is to first generate an unfolding of the net using the method of [AIN00] and then use a a SAT-solver to analyze the resulting unfolding. Our experiments show that the use of unfoldings, in spite of the two-step process, has better time and space characteristics than an implementation that does not use unfoldings. In effect, we provide the first evidence for the conjecture that the two step process based on unfoldings could be better than a single step verification process that considers all interleavings.
- SAT-based Analysis of Symbolic Unfoldings. [ANO01]
When applied to systems with a high amount of nondeterministic behaviour, SAT-based model checkers suffer from a formula explosion which limits their applicability to such systems. We describe an approach to limit the effects of formula explosion. We consider the technique of unfoldings and extend it to the context of SAT-based model checking. We apply the method to verify safety properties for systems which consist of finite-state concurrent processes operating on a set of Boolean variables. We show the applicability of the method through a number of experimental results.
Publications
You can find here a list of our published work.