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 Tutorial @ CADE 2021, July 11, 2021, Virtual.
• PVS Class 2012, October 9-12, 2012, Hampton, Virginia.
• LASER 2011: Advanced Theorem Proving Techniques in PVS and Applications.

PVS Packages for Verification Survival (PVS²)

The following PVS packages are either part of the current distribution of PVS or they are available from 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.
• Manip: A Strategy Package for PVS.
• Plaidypvs: Formal embedding of differential dynamic logic in the Prototype Verification System (PVS).
• 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.
• VSCode-PVS: A Visual Studio Code Extension for PVS.

Publications

• Laura Titolo, Mariano Moscato, Marco Feliu, Paolo Masci, and César Muñoz, Rigorous Floating-Point Round-Off Error Analysis in PRECiSA 4.0, Proceedings of the 26th International Symposium on Formal Methods (FM 2024), Lecture Notes in Computer Science, Vol. 12934, pp. 322-328. BibTeX Reference.
• J Tanner Slagel, Lauren White, Aaron Dutle, César Muñoz, and Nicolas Crespo, A Formal Verification Framework for Runtime Assurance, Proceedings of the 16th NASA Formal Methods Symposium (NFM 2024), Lecture Notes in Computer Science, Vol. 14627, pp. 322-328. BibTeX Reference.
• Lauren White, Laura Titolo, J. Tanner Slagel, and César Muñoz, A Temporal Differential Dynamic Logic Formal Embedding, Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2024), London, UK, 2024. BibTeX Reference.
• César Muñoz, Mauricio Ayala-Rincón, Mariano Moscato, Aaron Dutle, Anthony Narkawicz, Ariane Alves Almeida, Andréia B. Avelar, and Thiago M. Ferreira, Formal Verification of Termination Criteria for First-Order Recursive Functions, Journal of Automated Reasoning, Volume 67, Number 4, 2023. BibTeX Reference. This paper is an extended version of the conference publication in Schloss Dagstuhl - Leibniz- Zentrum für Informatik, Article No. 26, pp. 1-17, 2021.
• J. Tanner Slagel, Mariano Moscato, Lauren White, César Muñoz, Swee Balachandran, and Aaron Dutle, Embedding Differential Dynamic Logic in PVS, Proceedings of the 18th International Workshop on Logical and Semantic Frameworks, with Applications, 2023. Preprint.
• Lauren White, Laura Titolo, J. Tanner Slagel, Embedding Differential Temporal Dynamic Logic in PVS, Proceedings of the 29th International Conference on Types for Proofs and Programs TYPES 2023, 2023. Abstract.
• J. Tanner Slagel, César Muñoz, Swee Balachandran, Mariano M. Moscato, Aaron Dutle, Paolo Masci, and Lauren White, Towards an implementation of differential dynamic logic in PVS, Proceedings of the 11th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis (SOAP 2022), 2022.. BibTeX Reference.
• Víctor Carreño, Mariano M. Moscato, Paolo M. Masci, and Aaron Dutle, Interpretation and formalization of the right-of-way rules, Proceedings of 18th International Conference on Formal Aspects of Component Software (FAC 2022), Lecture Notes in Computer Science, Vol. 13712, pp. 59-73, 2022. BibTeX Reference.
• Paolo Masci and Aaron Dutle, Proof Mate: an Interactive Proof Helper for PVS (tool paper), Proceedings of the 14th NASA Formal Methods Symposium (NFM 2022), Lecture Notes in Computer Science, Vol. 13260, pp. 809-815, 2022. BibTeX Reference.
• Esther Conrad, Laura Titolo, Dimitra Giannakopoulou, Thomas Pressburger, and Aaron Dutle, A Compositional Proof Framework for FRETish Requirements, Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2022), 2022. BibTeX Reference.
• J. Tanner Slagel, Lauren White, and Aaron Dutle, Formal verification of semi-algebraic sets and real analytic functions, Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proof, pp. 278-290, 2021. BibTeX Reference.
• Aaron Dutle, Mariano Moscato, Laura Titolo, César Muñoz, Gregory Anderson, and François Bobot, Formal Analysis of the Compact Position Reporting Algorithm, Formal Aspects of Computing, Volume 33, Number 1, pp. 65-86, 2021. BibTeX Reference. This paper is an extended version of the conference publication in Lecture Notes in Computer Science, Vol. 10951, pp. 364-381, 2018.
• César Muñoz, Mauricio Ayala-Rincón, Mariano Moscato, Aaron Dutle, Anthony Narkawicz, Ariane Alves Almeida, Andréia B. Avelar, and Thiago M. Ferreira, Formal Verification of Termination Criteria for First-Order Recursive Functions, Proceedings of the 12th International Conference on Interactive Theorem Proving (ITP 2021), Article No. 26, pp. 1-17, Schloss Dagstuhl - Leibniz- Zentrum für Informatik, 2021. BibTeX Reference
• Katherine Cordwell, César Muñoz, and Aaron Dutle, Improving automated strategies for univariate quantifier elimination, Technical Memorandum, NASA/TM-20205010644, January 2021. BibTeX Reference.
• Laura Titolo, Mariano Moscato, Marco Feliú, and César Muñoz, Automatic Generation of Guard-Stable Floating-Point Code, Proceedings of the 16th International Conference on Integrated Formal Methods (iFM 2020), Lecture Notes in Computer Science, Vol. 12546, pp. 141–159, 2020. BibTeX Reference.
• Paolo Masci and César Muñoz, A Graphical Toolkit for the Validation of Requirements for Detect and Avoid Systems, Proceedings of the 14th International Conference on Tests and Proofs (TAP 2020), Lecture Notes in Computer Science, Vol. 12165, pp. 155-166, 2020. BibTeX Reference.
• Paolo Masci and César Muñoz, An Integrated Development Environment for the Prototype Verification System, Electronic Proceedings in Theoretical Computer Science, Vol. 310, pp. 35-49, 2019. BibTeX Reference.
• Mariano Moscato, Laura Titolo, Marco Feliú, and César Muñoz, Provably Correct Floating-Point Implementation of a Point-in-Polygon Algorithm, Proceedings of the 3rd World Congress on Formal Methods (FM 2019), Lecture Notes in Computer Science, Vol. 11800, pp. 21-37, 2019. BibTeX Reference.
• Rocco Salvia, Laura Titolo, Marco A. Feliú, Mariano M. Moscato, César Muñoz, and Zvonimir Rakamarić, A Mixed Real and Floating-Point Solver , Proceedings of the 11th NASA Formal Methods Symposium (NFM 2019), Lecture Notes in Computer Science, Vol. 11460, pp. 363-370, 2019. BibTeX Reference.
• John Siratt, Luis Crespo, Anthony Narkawicz, and César Muñoz, The Number of Support Constraints for Overlapping Set Optimization with Nested Admissible Sets is Equal to One, Technical Memorandum, NASA/TM-2018-220117, October 2018. BibTeX Reference.
• 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 Mendonç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.

News

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

Olds

• Hypatheon: Database capability for PVS theories.
• Practicals: High-level PVS tacticals.

The tag identifies links that are outside the NASA domain