Tags: Programming Language.
The Prototype Verification System (PVS) is a specification language integrated with support tools and an automated theorem prover developed at the Computer Science Laboratory of SRI International in Menlo Park California. PVS is based on a kernel consisting of an extension of Church’s theory of types with dependent types and is fundamentally a classical typed higher-order logic.