PVS Related Research Sponsored by NASA Langley

• Libraries ( Downloads)

  • 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.
  • 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.
  • Ricky W. Butler, Formalization of the Integral Calculus in the PVS Theorem Prover, NASA/TM-2004-213279, October 2004.
  • 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 ( Downloads)

  • 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.
  • Myla Archer, Ben Di Vito and César Muñoz, Editors, Design and Application of Strategies/Tactics in Higher Order Logics , NASA/CP-2003-212448, September 2003.
  • Cesar Munoz and Micela Mayero, Real Automation in the Field , NASA/CR-2001-211271, ICASE Interim Report 39, December 2001.

• Hypatheon

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

• Executable PVS

  • Cesar A. Munoz, Rapid Prototyping in PVS , NASA/CR-2003-212418; NIA Report 2003-03, December 2003.

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