Machine-Assisted Verification U sing Theorem Proving and Model Checking
N. Shankarl · 1997
Theorem proving and model checking are complementary ap proaches to the verification of hardware designs and software algorithms. In theorem proving, the verification task is one of showing that the formal de scription 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 spec ification and verification environment.