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.

- Anthony Narkawicz, César
Muñoz, and Aaron
Dutle,
*A Decision Procedure for Univariate Polynomial Systems Based on Root Counting and Interval Subdivision*, Journal of Formalized Reasoning, Vol. 11, Number 1, pp. 19-41, 2018. BibTeX Reference. - Thiago Mendoça Ferreira Ramos, César
Muñoz, Mauricio Ayala-Rincón, Mariano Moscato, Aaron
Dutle, and Anthony Narkawicz,
*Formalization of the Undecidability of the Halting Problem for a Functional Language*, Proceedings of the 25th Workshop on Logic, Language, Information, and Computation (WoLLIC 2018), Lecture Notes in Computer Science, Vol. 10944, pp. 196-209, 2018. BibTeX Reference. - Mariano Moscato, Carlos G. Lopez Pombo, César
Muñoz, and Marco Feliú,
*Boosting the Reuse of Formal Specifications*, Proceedings of the 9th International Conference on Interactive Theorem Proving (ITP 2018), Lecture Notes in Computer Science, Vol. 10895, pp. 477-494, 2018. BibTeX Reference. - César
Muñoz, Anthony Narkawicz, and Aaron
Dutle,
*From Formal Requirements to Highly Assured Software for Unmanned Aircraft Systems*, Proceedings of the 22nd International Symposium on Formal Methods (FM 2018) - Industry Day, Lecture Notes in Computer Science, Vol. 10951, pp. 647-652, 2018. BibTeX Reference. - Laura Titolo, Mariano Moscato, César
Muñoz, Aaron
Dutle, and François Bobot,
*A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm*, Proceedings of the 22nd International Symposium on Formal Methods (FM 2018), Lecture Notes in Computer Science, Vol. 10951, pp. 364-381, 2018. BibTeX Reference. - Laura Titolo, Marco Feliu, Mariano Moscato, and César
Muñoz,
*An Abstract Interpretation Framework for the Round-Off Error Analysis of Floating-Point Programs*, Proceedings 19th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2018), Lecture Notes in Computer Science, Vol. 10747, pp. 516-537, 2018. BibTeX Reference. - Aaron Dutle, Mariano Moscato, Laura Titolo, and César
Muñoz,
*A Formal Analysis of the Compact Position Reporting Algorithm*, Proceedings of the 9th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2017), Lecture Notes in Computer Science, Vol. 10712, pp. 19-34, 2017. BibTeX Reference. - Mariano Moscato, Laura Titolo, Aaron Dutle, and César
Muñoz,
*Automatic Estimation of Verified Floating-Point Round-Off Errors via Static Analysis*, Proceedings of the 36th International Conference on Computer Safety, Reliability and Security (SAFECOMP 2017), Lecture Notes in Computer Science, Vol. 10488, pp. 213-229, 2017. BibTeX Reference. - Anthony Narkawicz, César
Muñoz, and Aaron Dutle,
*The MINERVA Software Development Process*, Automated Formal Methods, Menlo Park, California, 2017. BibTeX Reference. - Camilo Rocha, José Meseguer, and César Muñoz,
*Rewriting Modulo SMT and Open System Analysis*, Journal of Logical and Algebraic Methods in Programming, Volume 86, Issue 1, pp. 269–297, 2017.. BibTeX Reference. This paper is an extended version of the conference publication in Lecture Notes in Computer Science, Vol. 8663, pp. 247-262, 2014. - 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.