PVS Related Research Sponsored by NASA Langley

• Libraries

  • NASA PVS Libraries
  • 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.
  • 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.
  • Marc Daumas, David Lester, and César Muñoz, Verified real number calculations: A library for interval arithmetic, IEEE Transactions on Computers, Volume 58, Number 2, 2009. BibTeX Reference.
  • Ricky Butler, Formalization of the Integral Calculus in the PVS Theorem Prover, Journal of Formalized Reasoning, Vol 2, No 1, 2009. Technical report available as: Ricky W. Butler, Formalization of the Integral Calculus in the PVS Theorem Prover, NASA/TM-2004-213279, October 2004.
  • Sylvie Boldo and César Muñoz, Provably Faithful Evaluation of Polynomials, Proceedings of the 21st Annual ACM Symposium on Applied Computing, 2006. BibTeX Reference.
  • Sylvie Boldo and César Muñoz, A High-Level Formalization of Floating-Point Numbers in PVS, NIA Report No. 2006-01, NASA/CR-2006-214298, 2006. BibTeX Reference.
  • César Muñoz and David Lester, Real Number Calculations and Theorem Proving, Proceedings of the 18th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2005, 2005. BibTeX Reference.
  • Marc Daumas, Guillaume Melquiond, and César Muñoz, Guaranteed Proofs Using Interval Arithmetic, Proceedings of the 17th IEEE Symposium on Computer Arithmetic ARITH-17, 2005. BibTeX Reference.
  • Myla Archer, Ben Di Vito, and César Muñoz, Developing User Strategies in PVS: A Tutorial, Proceedings of Design and Application of Strategies/Tactics in Higher Order Logics, STRATRA 2003, NASA/CP-2003-212448, 2003.
  • R. W. Butler and J. A. Sjogren, A PVS Graph Theory Library, NASA/TM-1998-206923, February 1998.
  • Ricky W. Butler, Paul S. Miner, Mandayam K. Srivas, Dave A. Greve, and Steven P. Miller, A Bitvectors Library for PVS, NASA TM-110274, August 1996.

• Strategies

  • 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.
  • Florent Kirchner and César Muñoz, PVS#: Streamlined Tacticals for PVS, Electronic Notes in Theoretical Computer Science, Volume 174, Issue 11, Page 47-58, July 2007. A draft version available here.
  • Ben L. Di Vito, A PVS Prover Strategy Package for Common Manipulations, NASA/TM-2002-211647, April 2002.
  • Ben L. Di Vito, Strategy-Enhanced Interactive Proving and Arithmetic Simplification for PVS, 1st International Workshop on Design and Application of Strategies/Tactics in Higher Order Logics (STRATA 2003), Roma, Italy, September 8, 2003.
  • César Muñoz and Micela Mayero, Real Automation in the Field, NASA/CR-2001-211271, ICASE Interim Report 39, December 2001. BibTeX Reference.

• Hypatheon

  • Overview of Project.
  • Ben Di Vito, Support Tools For PVS Theorem Proving

• PVS Development

  • César Muñoz, Batch Proving and Proof Scripting in PVS, NASA/CR-2007-214546, February 2007. BibTex Reference.
  • César Muñoz, Rapid Prototyping in PVS, NASA/CR-2003-212418, NIA Report 2003-03, December 2003. BibTeX Reference.
  • Myla Archer, Ben Di Vito, and César Muñoz, Developing User Strategies in PVS: A Tutorial, Proceedings of Design and Application of Strategies/Tactics in Higher Order Logics, STRATRA 2003, NASA/CP-2003-212448, 2003. BibTex Reference.
  • Gerald Lüttgen, César Muñoz, Ricky Butler, Ben Di Vito, and Paul Miner, Towards a customizable PVS, NASA/CR-2000-209851, ICASE Report 2000-04, January 2000. BibTex Reference.
  • César Muñoz and John Rushby, Structural Embeddings: Mechanization with Method, Proceedings of the World Congress on Formal Methods FM 99, 1999. BibTex Reference. Also available as ICASE Report 1999-26, July 1999. BibTex Reference.
  • Jean Paul Bodeveix, Mamoun Filali, and César Muñoz, A Formalization of the B-Method in Coq and PVS, Electronic Proceedings of the B-User Group Meeting at the World Congress on Formal Methods FM 99, 1999. BibTex Reference.

• Conference Proceedings

  • Otmane Ait Mohamed, César Muñoz, and Sofiène Tahar, Editors, Proceedings of the 21th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2008), Lecture Notes in Computer Science, Vol. 5170, 2008.
  • Myla Archer, Thierry Boy de la Tour, and César Muñoz, Proceedings of the 6th International Workshop on Strategies in Automated Deduction (STRATEGIES 2006), Electronic Notes in Theoretical Computer Science, Volume 174, Issue 11, 2007.
  • Myla Archer, Ben Di Vito, and César Muñoz, Editors, Proceedings of Design and Application of Strategies/Tactics in Higher Order Logics (STRATRA 2003), NASA/CP-2003-212448, September 2003.
  • Víctor Carreño, César Muñoz, and Sofiène Tahar, Editors, Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2002), Lecture Notes in Computer Science, Vol. 2410, 2002.

• SRI International

  • Sam Owre and Natarajan Shankar, Theory Interpretations in PVS, NASA/CR-2001-211024, July 2001, pp. 39.
  • Sam Owre and Natarajan Shankar, The Formal Semantics of PVS, NASA/CR-1999-209321, May 1999.
  • César Muñoz, PBS: Support for the B-Method in PVS, SRI Technical Report SRI-CSL-99-01, February 1999. BibTex Reference.
  • Sam Owre and Natarajan Shankar, Abstract Datatypes in PVS, NASA/CR-97-206264, November 1997.
  • Sam Owre, John Rushby and Natarajan Shankar, Analyzing Tabular and State-Transition Requirements Specifications in PVS, NASA CR-201729, July 1997.

Note: The tag identifies links that are outside of the NASA domain.