SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
  SRI Logo

Machine-Assited Verification Using Theorem Proving and Model Checking
 by Dr. Natarajan Shankar.

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.


About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2024 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy