Advanced Theorem Proving Techniques in PVS And Applications

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.

Pre-requisites:

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

Introductory Lectures (for reference only)

• 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

Lecture 0: Advanced Theorem Proving Techniques in PVS And Applications

• Lecture (Printer-friendly: letter, a4)

Lecture 1: PVS for the Impatient

• Lecture (Printer-friendly: letter, a4)
• Examples
• Exercises

Lecture 2: Recursion, Induction, and Other Demons

• Lecture (Printer-friendly: letter, a4)
• Examples
• Exercises

Lecture 3: Real Applications

• Lecture (Printer-friendly: letter, a4)
• Examples
• Exercises

Advanced Lectures

• 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)

Challenge Problems and Solutions

• Solutions to Exercises
• Queens (Proof file)
• Absolute Value on 2's Complement Integers (Proof file)

The tag identifies links that are outside the NASA domain