Abstract
The Prototype Verification System (PVS) is an interactive verification environment that combines a strongly typed specification language with a classical higher-order logic theorem prover. The PVS type system supports: predicate subtypes, dependent types, abstract data types, compound types such as records, unions, and tuples, and basic types such as numbers, Boolean values, and strings. The PVS theorem prover includes decision procedures for a variety of theories such as linear arithmetic, propositional logic, and temporal logic. This paper surveys advanced PVS features, including: types for specifications, implicit induction, iterations, rapid prototyping, strategy writing, and computational reflection. These features are illustrated with simple examples taken from NASA PVS developments.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Archer, M., Vito, B.D., Muñoz, C.: Developing user strategies in PVS: A tutorial. In: Proceedings of Design and Application of Strategies/Tactics in Higher Order Logics STRATA 2003. NASA/CP-2003-212448, NASA LaRC, Hampton VA 23681-2199, USA (September 2003)
Crow, J., Owre, S., Rushby, J., Shankar, N., Stringer-Calvert, D.: Evaluating, testing, and animating PVS specifications. Tech. rep., Computer Science Laboratory, SRI International, Menlo Park, CA (March 2001)
Daumas, M., Lester, D., Muñoz, C.: Verified real number calculations: A library for interval arithmetic. IEEE Transactions on Computers 58(2), 226–237 (2009)
Di Vito, B.: A PVS prover strategy package for common manipulations. Technical Memorandum NASA/TM-2002-211647, NASA Langley Research Center (2002)
Harrison, J.: Metatheory and reflection in theorem proving: A survey and critique. Technical Report CRC-053, SRI Cambridge, Millers Yard, Cambridge, UK (1995)
Lensink, L., Smetsers, S., van Eekelen, M.: Generating Verifiable Java Code from Verified PVS Specifications. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 310–325. Springer, Heidelberg (2012)
Lüttgen, G., Muñoz, C., Butler, R., Vito, B.D., Miner, P.: Towards a customizable PVS. Contractor Report NASA/CR-2000-209851, ICASE, Langley Research Center, Hampton VA 23681-2199, USA (January 2000)
Manolios, P., Vroon, D.: Termination Analysis with Calling Context Graphs. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 401–414. Springer, Heidelberg (2006)
Muñoz, C.: Rapid prototyping in PVS. Contractor Report NASA/CR-2003-212418, NASA, Langley Research Center, Hampton VA 23681-2199, USA (May 2003)
Muñoz, C.: Batch proving and proof scripting in PVS. Report NIA Report No. 2007-03, NASA/CR-2007-214546, NIA-NASA Langley, National Institute of Aerospace, Hampton, VA (February 2007)
Muñoz, C., Mayero, M.: Real automation in the field. Contractor Report NASA/CR-2001-211271, ICASE, Langley Research Center, Hampton VA 23681-2199, USA (December 2001)
Muñoz, C., Narkawicz, A.: Formalization of a representation of Bernstein polynomials and applications to global optimization. Journal of Automated Reasoning (2012) (accepted for publication)
Nipkow, S.B.T.: Random testing in Isabelle/HOL. In: Cuellar, J., Liu, Z. (eds.) Software Engineering and Formal Methods (SEFM 2004), pp. 230–239. IEEE Computer Society (2004)
Owre, S., Rushby, J., Shankar, N.: PVS: A Prototype Verification System. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748–752. Springer, Heidelberg (1992)
Owre, S., Shankar, N.: Abstract datatypes in PVS. Contractor Report NASA/CR-97-206264, NASA, Langley Research Center, Hampton VA 23681-2199, USA (November 1997)
Owre, S., Shankar, N.: The formal semantics of PVS. Technical Report CSL-97-2, Computer Science Laboratory, SRI International (March 1999)
Owre, S., Shankar, N.: Theory interpretations in PVS. Technical report, SRI International, Menlo Park, CA (April 2001)
Rushby, J., Owre, S., Shankar, N.: Subtypes for specifications: Predicate subtyping in PVS. IEEE Transactions on Software Engineering 24(9), 709–720 (1998), http://www.csl.sri.com/papers/tse98/
Shankar, N.: Efficiently executing PVS. Technical report, Computer Science Laboratory, SRI International, Menlo Park, CA (November 1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Muñoz, C.A., Demasi, R.A. (2012). Advanced Theorem Proving Techniques in PVS and Applications. In: Meyer, B., Nordio, M. (eds) Tools for Practical Software Verification. LASER 2011. Lecture Notes in Computer Science, vol 7682. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35746-6_4
Download citation
DOI: https://doi.org/10.1007/978-3-642-35746-6_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-35745-9
Online ISBN: 978-3-642-35746-6
eBook Packages: Computer ScienceComputer Science (R0)