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.
- 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. 14934,
pp. 20-38. BibTeX
Reference.
- J Tanner Slagel, Lauren M. White, Aaron Dutle, César Muñoz, and
Nicolas Crespo,
A verification framework for runtime assurance of autonomous UAS,
Proceedings of the 43rd Digital Avionics Systems Conference (DASC 2024),
September-October 2024, San Diego, CA, USA. 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
Olds
The tag
identifies links that are outside
the NASA domain