NASA logo

+ Contact NASA

  • + HOME
  • + TEAM
  • + LINKS

  • Theorem Proving Research Sponsored by NASA

    The Program Verification System[*] (PVS) is a formal verification system developed by SRI International[*]. PVS provides a rich specification language based on a strongly-typed higher-order logic and a powerful theorem prover for this logic. The PVS type system supports sub-typing and dependent types. The theorem prover includes decision procedures and simplification strategies for a variety of theories.

    PVS is key component of several formal verification projects at NASA Langley. For that reason, NASA Langley supports a PVS Research effort that aims at the advancement of theorem proving techniques for complex safety-critical applications. The Formal Methods group at NASA Langley, in collaboration with the PVS community, develops and maintains the NASA PVS Library, a large collection of PVS developments that range from fundamental mathematical theories to frameworks for the verification of air traffic systems and fault-tolerant protocols. The NASA PVS Library is featured in the movie “The Martian”.

    PVS Tutorials

    PVS Packages for Verification Survival (PVS2)

    The following PVS packages are either part of the current distribution of PVS[*] or they are available from the NASA PVS Library.




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