At a Glance
| Applications | Theorem Prover |
| Developers | SRI International |
| Inputs | PVS |
| Interfaces | CLI GUI |
| Licenses | GPL-2.0 |
| Maintenance | Actively Maintained |
Description
PVS is a mechanized environment for formal specification and verification. PVS consists of a specification language, a large number of predefined theories, a type checker, an interactive theorem prover that supports the use of several decision procedures and a symbolic model checker, various utilities including a code generator and a random tester, documentation, formalized libraries, and examples that illustrate different methods of using the system in several application areas.