PVS is a specification and verification system that combines an expressive specification language with support tools and an interactive theorem prover. It provides a mechanised environment for developing formal specifications and constructing and checking proofs.
The specification language is based on higher-order logic and supports predicate subtypes, dependent types, recursive datatypes, and parameterised theories. PVS integrates type checking with powerful proof automation and decision procedures.
This is free and open source software.
Key Features
- Expressive specification language based on higher-order logic.
- Interactive theorem prover with automated deduction capabilities.
- Predicate subtypes and dependent types.
- Recursive datatypes and parameterised theories.
- Type checker that generates proof obligations.
- Decision procedures for equality and linear arithmetic.
- Supports induction, rewriting, and simplification.
- Symbolic model checking.
- Proof scripts can be edited and rerun.
- Batch and headless operation.
- Code generation and random testing utilities.
- Extensive predefined theories, libraries, and examples.
Website: github.com/SRI-CSL/PVS
Support:
Developer: SRI International Computer Science Laboratory
License: BSD 3-Clause “New” or “Revised” License
PVS is written in Common Lisp. Learn Lisp with our recommended free books and free tutorials.
Related Software
| Proof Assistants | |
|---|---|
| Coq | Formal proof management system |
| Isabelle | Generic proof assistant; express mathematical formulas in a formal language |
| Agda | Interactive system for writing and checking proofs |
| Lean | Programming language and theorem prover |
| Matita | Experimental, interactive theorem prover |
Read our verdict in the software roundup.
 Explore our comprehensive directory of recommended free and open source software. Our carefully curated collection spans every major software category.This directory is part of our ongoing series of informative articles for Linux enthusiasts. It features hundreds of detailed reviews, along with open source alternatives to proprietary solutions from major corporations such as Google, Microsoft, Apple, Adobe, IBM, Cisco, Oracle, and Autodesk. You’ll also find interesting projects to try, hardware coverage, free programming books and tutorials, and much more. Discovered a useful open source Linux program that we haven’t covered yet? Let us know by completing this form. |