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

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

- Affine: Affine arithmetic and proof-producing strategy for evaluating polynomials with variables on interval domains.
- Bernstein: Formalization of multivariate polynomial global optimization algorithms using Bernstein polynomials.
- Extrategies: Strategy combinators for writting strategies.
- Field: Simplification strategies for real number expressions.
- Kodiak: C++ implemenation of a formally-verified branch and bound algorithm.
- Interval: Interval arithmetic and proof-producing strategies for reasoning about real-valued expressions.
- ProofLite: Batch proving and proof scripting.
- PVSio: Animation and rapid prototyping.
- Sturm: Formalization of Sturm's Theorem and proof-producing strategies for reasoning about univariate polynomial relations over a real interval.
- Tarski: Formalization of Tarski's Theorem and proof-producing strategy for reasoning about systems of univariate polynomial relations.

- César Muñoz, Aaron Dutle, Anthony Narkawicz, and
Jason Upchurch,
*Unmanned Aircraft Systems in the National Airspace System: A Formal Methods Perspective*, ACM SIGLOG News, Vol. 3. Number 3, pp. 67-76, 2016. BibTeX Reference. - César Muñoz and Anthony Narkawicz,
*Formal analysis of extended well-clear boundaries for unmanned aircraft*, Proceedings of the 8th NASA Formal Methods Symposium (NFM 2016), Lecture Notes in Computer Science, Vol. 9690, pp. 221-226, 2016. BibTeX Reference. *Formal Methods in Air Traffic Management: The Case of Unmanned Aircraft Systems (Invited Lecture)*, Proceedings of the 12th International Colloquium on Theoretical Aspects of Computing (ICTAC 2015), Lecture Notes in Computer Science, Vol. 9399, pp. 58-62, 2015. BibTeX Reference.- Mariano Moscato, César Muñoz, and Andrew Smith,
*Affine Arithmetic and Applications to Real-Number Proving*, Proceedings of the 6th International Conference on Interactive Theorem Proving (ITP 2015), Lecture Notes in Computer Science, Vol. 9236, pp. 294-309, 2015. BibTeX Reference. - Andrew Smith, César Muñoz, Anthony Narkawicz, and
Mantas Markevicius,
*Kodiak: An Implementation Framework for Branch and Bound Algorithms*, Technical Memorandum, NASA/TM-2015-218776, July 2015. BibTeX Reference. - Aaron Dutle, César Muñoz, Anthony Narkawicz, and
Ricky Butler,
*Software Validation via Model Animation*, Proceedings of the Proceedings of the 9th International Conference on Tests and Proofs (TAP 2015), Lecture Notes in Computer Science, Vol. 9154, pp. 92-108, 2015. BibTeX Reference. - Anthony Narkawicz, César Muñoz, and Aaron Dutle,
*Formally-Verified Decision Procedures for Univariate Polynomial Computation Based on Sturm’s and Tarski’s Theorems*, Journal of Automated Reasoning, Volume 54, Issue 4, pp. 285-326, 2015. DOI: 10.1007/s10817-015-9320-x. BibTeX Reference. - Anthony Narkawicz and César Muñoz,
*A Formally-Verified Decision Procedure for Univariate Polynomial Computation Based on Sturm’s Theorem*, Technical Memorandum, NASA/TM-2014-218548, November 2014. BibTeX Reference. - Camilo Rocha, José Meseguer, and César Muñoz,
*Rewriting Modulo SMT and Open System Analysis*, Proceedings of the 10th International Workshop on Rewriting Techniques and Applications (WRLA2014), Lecture Notes in Computer Science, Vol. 8663, pp. 247-262, 2014. BibTeX Reference. - William Denman and César Muñoz,
*Automated Real Proving in PVS via MetiTarski*, Proceedings of the 19th International Symposium on Formal Methods (FM 2014), Lecture Notes in Computer Science, Vol. 8442, pp. 194-199, 2014. BibTeX Reference. - Anthony Narkawicz and César Muñoz,
*A Formally Verified Generic Branching Algorithm for Global Optimization*, Proceedings of the Fifth Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE 2013), Lecture Notes in Computer Science, Vol. 8164, pp. 326-343, 2014. BibTeX Reference. - Camilo Rocha and César Muñoz,
*Synchronous set relations in rewriting logic*, Science of Computer Programming, Volume 92, Part B, pp. 211-228, 2014. BibTeX Reference. - Camilo Rocha, José Meseguer, and César Muñoz,
*Rewriting Modulo SMT*, Technical Memorandum, NASA/TM-2013-218033, August 2013. BibTeX Reference. - César Muñoz and Anthony Narkawicz,
*Formalization of a Representation of Bernstein Polynomials and Applications to Global Optimization*, Journal of Automated Reasoning, Volume 51, Issue 2, pp. 151-196, 2013. BibTeX Reference. - Camilo Rocha and César Muñoz,
*Simulation and Verification of Synchronous Set Relations in Rewriting Logic*, Proceedings of 14th Brazilian Symposium on Formal Methods (SBMF 2011), Lecture Notes in Computer Science, Volume 7021, pp. 60-75, September 2011. BibTeX Reference. - Camilo Rocha, César Muñoz, and Gilles Dowek,
*A Formal Library of Set Relations and Its Application to Synchronous Languages*, Theoretical Computer Science, Volume 412, Issue 37, pp. 4853-4866, August 2011. BibTeX Reference. - Alwyn Goodloe and César Muñoz,
*Compositional Verification of a Communication Protocol for a Remotely Operated Aircraft*, Science of Computer Programming, Volume 78, Issue 7, pp. 813-827, 2013. BibTeX Reference. This paper is an extended version of the conference publication in Lecture Notes in Computer Science, Volume 5825, November 2009. - Anthony Narkawicz, Jürgen Garloff, Andrew Smith, and César
Muñoz,
*Bounding the Range of a Rational Function over a Box*, Reliable Computing, Volume 17, pp. 209-237, December, 2012. BibTeX Reference. - César Muñoz and Ramiro Demasi,
*Advanced Theorem Proving Techniques in PVS and Applications*, Tools for Practical Software Verification - LASER 2011, International Summer School, Lecture Notes in Computer Science, Volume 7682, pp. 97-133, 2012. BibTeX Reference. - The 2012 CAV (Computer-Aided Verification) Award was presented to Sam Owre, John Rushby, and Natarajan Shankar of SRI International for the development of PVS.
- PVS Class 2012, October 9-12, 2012, Hampton, Virginia.
- LASER 2011: Advanced Theorem Proving Techniques in PVS and Applications.

- Practicals: High-level tacticals.