NASA logo

+ Contact NASA

  • + HOME
  • + TEAM
  • + LINKS

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


    Introductory Lectures (for reference only)

    Lecture 0: Advanced Theorem Proving Techniques in PVS And Applications

    Lecture 1: PVS for the Impatient

    Lecture 2: Recursion, Induction, and Other Demons

    Lecture 3: Real Applications

    Advanced Lectures

    Challenge Problems and Solutions

    The tag [*] identifies links that are outside the NASA domain