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.

- PVS 5.0 (Allegro binaries are strongly suggested)
- NASA PVS Libraries

- Expression Language by B. Di Vito
- Type Declarations by B. Di Vito
- Propositional Logic Proving by B. Di Vito
- Predicate Logic Proving by P. Miner
- Advance Type Features by J. Maddalon
- Collections by J. Maddalon
- Abstract Data Types by P. Miner

- Batch Proving (Printer-friendly: letter, a4; Examples)
- Theory Interpretations (Printer-friendly: letter, a4; Examples)
- Rapid Prototyping (Printer-friendly: letter, a4; Examples)
- Strategy Writing (Printer-friendly: letter, a4; Examples)