These lectures were prepared by César Muñoz, in collaboration with the NASA Langley Formal Methods Group, for the 8th LASER Summer School on Software Engineering: Tools for Practical Software Verification.
The Prototype Verification System (PVS) is an
interactive environment for the specification and verification of
systems. PVS provides a strongly typed specification language, which
is based on Higher-Order Logic. The type system of PVS supports:
sub-typing, dependent-types, abstract data types, parametric types,
records, unions, and tuples. The PVS theorem prover includes decision
procedures for a variety of theories such as linear arithmetic,
propositional logic, and temporal logic. The Formal Methods group at
NASA Langley develops and applies PVS theorem proving technology for
verification of safety-critical aerospace applications. This seminar
will provide a gentle introduction to advanced PVS features,
including: theory interpretations, real number proving, implicit
induction, batch proving, rapid prototyping, and strategy development.
All of these features are illustrated with examples taken from
verification research at NASA.