Paper Info
Title
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.
Year
DOI
Venue
2008
10.1007/978-3-540-71067-7_5
TPHOLs
Keywords
Field
DocType
ground evaluation,corecursive datatypes,illustrative example,decision procedure,predicate abstraction,brief overview,automatic simplification,predicate subtypes,pvs application,coinductive definition,model checking,random testing
Programming language,Model checking,Predicate abstraction,Computer science,Algorithm,Binary tree,Theoretical computer science,Coinduction,Rewriting,Predicate (grammar),Gas meter prover,Recursion
Conference
Volume
ISSN
Citations 
5170
0302-9743
12
PageRank 
References 
Authors
0.64
11
2
Name
Order
Citations
PageRank
Sam Owre11323104.39
Natarajan Shankar23050309.55