Advertisement
Published in:
2012 | OriginalPaper | Chapter
Advanced Theorem Proving Techniques in PVS and Applications
Authors : César A. Muñoz, Ramiro A. Demasi
Published in: Tools for Practical Software Verification
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
The Prototype Verification System (PVS) is an interactive verification environment that combines a strongly typed specification language with a classical higher-order logic theorem prover. The PVS type system supports: predicate subtypes, dependent types, abstract data types, compound types such as records, unions, and tuples, and basic types such as numbers, Boolean values, and strings. The PVS theorem prover includes decision procedures for a variety of theories such as linear arithmetic, propositional logic, and temporal logic. This paper surveys advanced PVS features, including: types for specifications, implicit induction, iterations, rapid prototyping, strategy writing, and computational reflection. These features are illustrated with simple examples taken from NASA PVS developments.