Symbolic model checking is PSPACE complete. Since QBF is the standard
PSPACE complete problem, it is most natural to encode symbolic model
checking problems as QBF formulas and then use QBF decision procedures
to solve them. We discuss alternative encodings for unbounded and
bounded safety checking into SAT and QBF. One contribution is a linear
encoding of simple path constraints, which usually are necessary to
make $k$-induction complete. Our experimental results show that indeed a
large reduction in the size of the generated formulas can be obtained.
However, current QBF solvers seem not to be able to take advantage of
these compact formulations. Despite these mostly negative results the
availability of these benchmarks will help improve the state of the art
of QBF solvers and make QBF based symbolic model checking a viable
alternative.
| Original language | English |
|---|
| Title of host publication | Proc. 4th Intl. Workshop on Bounded Model Checking (BMC'06), Seattle, USA |
|---|
| Number of pages | 14 |
|---|
| Publication status | Published - 2006 |
|---|
| Name | Electronic Notes in Theoretical Computer Science (ENTCS) |
|---|
- 102 Computer Sciences
- 101013 Mathematical logic