-
Notifications
You must be signed in to change notification settings - Fork 32
Home
The Prototype Verification System (PVS) is a tool for the analysis of hardware and software components of safety-critical systems. The tool provides an expressive specification language integrated with a simulation environment, and an automated 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.
PVS 6.0 is the current stable version of the tool. It is a significant new release of PVS, with several new features and improvements. The highlights include:
- Declaration parameters for the definition of generic theories
- Improved numeric simplification for all arithmetic operators
- Unicode character support
- Full integration of the NASA packages PVSio, ProofLite, Field, and Manip
- Improved theory interpretation mechanism
You can download PVS 6.0 from our servers, but you must must read and accept the click-through license that comes up when you choose the download.
To effectively use PVS, you should at least get the System Guide, Language Reference, and Prover Guide. The semantics report provides the semantics for the core of PVS, the datatypes report provides details and examples that go beyond what is described in the language manual, and theory interpretations describes the recently introduced capabilities supporting refinement and consistency. The release notes present the new advanced features introduced over the years in the new releases of PVS.