ACL2 Seminar, Feb. 5, 2013
Programming and Proving with  PVS
Natarajan Shankar, SRI International Computer Science Laboratory

SRI's Prototype Verification System (PVS) is an interactive theorem
proving framework based on higher-order logic.  It was first released
twenty years ago.  The original version of PVS featured several novel
features including an extension of higher-order logic with predicate
subtypes, dependent types, and parametric theories, and an integration
of decision procedures with interactive theorem proving.  Over the
years, new features have been added, such as an integration of
mu-calculus model checking, predicate abstraction, several external
decision procedures, theory interpretations, codatatypes and
corecursion, and efficient code generation.  PVS has been used
directly for proof development and as a back-end to other tools
through semantic embeddings.  The language and proof features have
demonstrated their value over a large body of proofs.  We present a
quick overview of some of the features of PVS, and briefly discuss
our future plans.