Theorem proving and model checking are complementary approaches to the verification of hardware designs and software algorithms. In theorem proving, the verification task is one of showing that the formal description of the program implies the formal statement of a putative program property, while model checking demonstrates that the program is a model that satisfies the putative property. Theorem proving is completely general but typically requires significant human guidance, whereas model checking though restricted to a limited range of properties of small (essentially) finite state systems, is largely automatic. This paper is a tutorial on the combined use of theorem proving and model checking as mechanized in the PVS specification and verification environment.

• marktoberdorf96.ps