PVS is an automated tool for specification and verification that is designed to exploit the synergies between language and deduction, automation and interaction, and theorem proving and model checking. PVS strives for a balance between automation and interaction by using decision procedures to simplify the tedious and obvious steps in a proof leaving the user to interactively supply the high-level steps in a verification. Decision procedures for BDD-based propositional simplification and model checking, equality, and linear arithmetic are integrated into PVS. The utility of the language and deductive features of PVS have been demonstrated in a number of examples, including the specification and partial verification of the Rockwell-Collins AAMP5 processor design [9], and the verification of an SRT divider [13]. This tutorial concentrates on the integration of individual verification techniques available in PVS.

• fmcad96-shankar.ps