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