

home >
research >
PVS related
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. 326343, 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. 151196, 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/TM2004213279, 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 HighLevel Formalization of FloatingPoint Numbers in PVS,
NIA Report No. 200601, NASA/CR2006214298, 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 ARITH17, 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/CP2003212448, 2003.
 R. W. Butler and J. A. Sjogren,
A PVS Graph Theory Library,
NASA/TM1998206923, February 1998.
 Ricky W. Butler, Paul S. Miner, Mandayam K. Srivas, Dave A. Greve, and Steven P. Miller,
A Bitvectors Library for PVS,
NASA TM110274, 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. 194199, 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 4758, July 2007. A draft version available here.
 Ben L. Di Vito,
A PVS Prover Strategy Package for Common Manipulations,
NASA/TM2002211647, April 2002.
 Ben L. Di Vito,
StrategyEnhanced 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/CR2001211271, ICASE Interim Report 39, December 2001. BibTeX Reference.

Hypatheon

PVS Development
 César Muñoz, Batch Proving and Proof Scripting in PVS, NASA/CR2007214546,
February 2007. BibTex
Reference.
 César Muñoz,
Rapid Prototyping in PVS,
NASA/CR2003212418, NIA Report 200303, 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/CP2003212448, 2003.
BibTex Reference.
 Gerald Lüttgen, César Muñoz, Ricky Butler,
Ben Di Vito, and Paul Miner, Towards a customizable PVS,
NASA/CR2000209851, ICASE Report 200004, 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 199926,
July 1999. BibTex
Reference.
 Jean Paul Bodeveix, Mamoun Filali, and César Muñoz, A
Formalization of the BMethod in Coq and PVS,
Electronic Proceedings
of the BUser 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/CP2003212448, 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/CR2001211024, July 2001, pp. 39.
 Sam Owre and Natarajan Shankar,
The Formal Semantics of PVS,
NASA/CR1999209321, May 1999.
 César Muñoz, PBS: Support for the BMethod
in PVS,
SRI Technical Report
SRICSL9901, February 1999. BibTex Reference.
 Sam Owre and Natarajan Shankar,
Abstract Datatypes in PVS,
NASA/CR97206264, November 1997.
 Sam Owre, John Rushby and Natarajan Shankar,
Analyzing Tabular and StateTransition Requirements Specifications in PVS,
NASA CR201729, July 1997.
Note: The
tag identifies links that are outside of the NASA domain.
