4th Intl. Workshop on Bounded Model Checking (BMC'06),
Sprache des Tagungstitel:
Englisch
Original Kurzfassung:
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.
Forschungs-