A Brief Overview of PVS

Abstract

PVS is now 15 years old, and has been extensively used in research, industry, and teaching. The system is very expressive, with unique features such as predicate subtypes, recursive and corecursive datatypes, inductive and coinductive definitions, judgements, conversions, tables, and theory interpretations. The prover supports a combination of decision procedures, automatic simplification, rewriting, ground evaluation, random test case generation, induction, model checking, predicate abstraction, MONA, BDDs, and user-defined proof strategies. In this paper we give a very brief overview of the features of PVS, some illustrative examples, and a summary of the libraries and PVS applications.

PDF PS

Slides

PDF

BibTeX Entry

@inproceedings{PVSTUT:TPHOLS08,
	AUTHOR = {Sam Owre and N. Shankar},
	TITLE = {A Brief Overview of {PVS}},
        BOOKTITLE = {Theorem Proving in Higher Order Logics, TPHOLs 2008},
	EDITOR = {Otmane Ait Mohamed and C\'{e}sar Mu\~{n}oz and Sofi\'{e}ne Tahar},
	PAGES = {22--27},
        MONTH = aug,
        YEAR = 2008,
        PUBLISHER = {Springer-Verlag},
        ADDRESS = {Montreal, Canada},
        SERIES = {Lecture Notes in Computer Science},
	VOLUME = 5170
}
Sam Owre: owre@csl.sri.com