[PDF][PDF] Efficient generation of counterexamples and witnesses in symbolic model checking

EM Clarke, O Grumberg, KL McMillan… - Proceedings of the 32nd …, 1995 - dl.acm.org
Proceedings of the 32nd annual ACM/IEEE Design Automation Conference, 1995dl.acm.org
Abstract Model checking is an automatic technique for verifying sequential circuit designs
and protocols. An ecient search procedure is used to determine whether or not the speci
cation is satis ed. If it is not satis ed, our technique will produce a counterexample execution
trace that shows the cause of the problem. We describe an e cient algorithm to produce
counterexamples and witnesses for symbolic model checking algorithms. This algorithm is
used in the SMV model checker and works quite well in practice. We also discuss how to …
Abstract
Model checking is an automatic technique for verifying sequential circuit designs and protocols. An ecient search procedure is used to determine whether or not the speci cation is satis ed. If it is not satis ed, our technique will produce a counterexample execution trace that shows the cause of the problem. We describe an e cient algorithm to produce counterexamples and witnesses for symbolic model checking algorithms. This algorithm is used in the SMV model checker and works quite well in practice. We also discuss how to extend our technique to more complicated speci cations.
ACM Digital Library