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. © 2008 Springer Berlin Heidelberg.
Cite
CITATION STYLE
Owre, S., & Shankar, N. (2008). A brief overview of PVS. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5170 LNCS, pp. 22–27). Springer Verlag. https://doi.org/10.1007/978-3-540-71067-7_5
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
