A Tutorial on Using PVS for Hardware Verification

PVS stands for "Prototype Verification System." It consists of a specification language integrated with support tools and a theorem prover. PVS tries to provide the mechanization needed to apply formal methods both rigorously and productively. This tutorial serves to introduce PVS and its use in the context of hardware verification. In the first section, we briefly sketch the purposes for which PVS is intended and the rationale behind its design, mention some of the uses that we and others are making of it. We give an overview of the PVS specification language and proof checker. The PVS language, system, and theorem prover each have their own reference manuals, which you will need to study in order to make productive use of the system. A pocket reference card, summarizing all the features of the PVS language, system, and prover is also available. The purpose of this tutorial is not to describe in detail the features of PVS and how to use the system. Rather, its purpose is to..