PVS is a verification system: that is, a specification language integrated with support tools and a theorem prover. It is intended to capture the state of the art in mechanized formal methods and to be sufficiently rugged that it can be used for significant applications. PVS is a research prototype: it evolves and improves as we develop or apply new capabilities, and as the stress of real use exposes new requirements.

More Information: http://pvs.csl.sri.com/

• Dr. John Rushby

• Dr. Patrick Lincoln
• Sam Owre
• Dr. Natarajan Shankar
• Dr. Ashish Tiwari

• Formal Verification of Functional Properties of an SCR-Style Software Requirements Specification Using PVS  (2002)
• Integrating WS1S with PVS  (2000)
• Principles and Pragmatics of Subtyping in PVS  (1999)
• The Formal Semantics of PVS  (1999)
• Systematic Formal Verification for Fault-Tolerant Time-Triggered Algorithms (1999)  (1999)
• Abstract and Model Check while you Prove  (1999)
• Subtypes for Specifications: Predicate Subtyping in PVS  (1998)
• PVS: An Experience Report  (1998)
• Fair Synchronous Transition Systems and their Liveness Proofs  (1998)
• Ubiquitous Abstraction: A New Approach for Mechanized Formal Verification (Extended Abstract)  (1998)
• Towards Light-Weight Verication and Heavy-Weight Testing  (1998)
• Integration in PVS: Tables, Types, and Model Checking  (1997)
• Systematic Formal Verification for Fault-Tolerant Time-Triggered Algorithms (1997)  (1997)
• Subtypes for Specifications  (1997)
• Steps Towards Mechanizing Program Transformations Using PVS  (1996)
• PVS: Combining Specification, Proof Checking, and Model Checking  (1996)
• A Less Elementary Tutorial for the PVS Specification and Verification System  (1995)
• A Tutorial Introduction to PVS  (1995)
• Analyzing Tabular and State-Transition Specifications in PVS  (1995)
• Model Checking and Other Ways of Automating Formal Methods  (1995)
• A Tutorial on Using PVS for Hardware Verification  (1994)
• Formal Verification of an Interactive Consistency Algorithm for the Draper FTP Architecture Under a Hybrid Fault Model  (1994)
• Effective Theorem Proving for Hardware Verification  (1994)
• The Formal Verification of an Algorithm for Interactive Consistency under a Hybrid Fault Model  (1993)
• Formal Verification for Fault-Tolerant Architectures: Some Lessons Learned  (1993)
• Using PVS to Prove Some Theorems of David Parnas  (1993)
• Verification of Real-Time Systems Using PVS  (1993)
• Formal Verification of an Oral Messages Algorithm for Interactive Consistency  (1992)
• PVS: A Prototype Verification System  (1992)
• Deconstructing Shostak