Abstract
PVS is a comprehensive interactive tool for specification and verification combining an expressive specification language with an integrated suite of tools for theorem proving and model checking. PVS has many academic and industrial users and has been applied to a wide range of verification tasks. In this note, we summarize some of its applications.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
The development of PVS was funded by SRI International through Internal R&D funds. Various applications and customizations have been funded by NSF Grants CCR-930044 and CCR-9509931, and by contracts F49620-95-C0044 from AFOSR, NAS1-20334 from NASA, and N00015-92-C-2177 from NRL.
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
Parosh Aziz Abdulla, Aurore Annichini, Saddek Bensalem, Ahmed Bouajjani, Peter Habermehl, and Yassine Lakhnech. Verification of infinite-state systems by combining abstraction and reachability analysis. In CAV’99 [8].
Andren Alborghetti, Angelo Gargantini, and Angelo Morzenti. Providing auto mated support to deductive analysis of time critical systems. In Mehdi Jazayeri and Helmut Schauer, editors, Software Engineering-ESEG/FSE’ 97: Sixth European Software Engineering Conference and Fifth ACM SIGSOFT Symposium on the Foundations of Software Engineering, volume 1301 of Lecture Notes in Computer Science, pages 211–226, Zurich, Switzerland, September 1997. Springer-Verlag.
Rajeev Alur and Thomas A. Henzinger, editors. Computer-Aided Verification, CAV’ 96, volume 1102 of Lecture Notes in Computer Science, New Brunswick, NJ, July/August 1996. Springer-Verlag.
Myla Archer and Constance Heitmeyer. Mechanical verification of timed au tomata: A case study. In IEEE Real-Time Technology and Applications Symposium (RTAS’96), pages 192–203, Brookline, MA, June 1996. IEEE Computer Society.
Saddek Bensalem, Yassine Lakhnech, and Hassen Saïdi. Powerful techniques for the automatic generation of invariants. In Thomas A. Henzinger, editors. Computer-Aided Verification, CAV’ 96, volume 1102 of Lecture Notes in Computer Science, New Brunswick, NJ, July/August 1996 Alur and Henzinger [3], pages 323–335.
Bettina Buth. PAMELA + PVS. In Michael Johnson, editor, Algebraic Methodology and Software Technology, AMAST’97, volume 1349 of Lecture Notes in Computer Science, pages 560–562, Sydney, Australia, December 1997. Springer-Verlag.
Ricky W. Butler and Jon A. Sjogren. A PVS graph theory library. NASA Technical Memorandum 1998-206923, NASA Langley Research Center, Hampton, VA, February 1998.
Computer-Aided Verification, CAV’ 99, Lecture Notes in Computer Science, Trento, Italy, July 1999. Springer-Verlag. To appear.
Raphael Couturier and Dominique Méry. An experiment in parallelizing an appli cation using formal methods. In Moshe Y. Vardi, editors. Computer-Aided Verification, CAV’ 98, volume 1427 of Lecture Notes in Computer Science, Vancouver, Canada, June 1998 Hu and Vardi [25], pages 345–356.
Judith Crow and Ben L. Di Vito. Formalizing Space Shuttle software requirements: Four case studies. ACM Transactions on Software Engineering and Methodology, 7(3):296–332, July 1998.
Drew Dean. Static typing with dynamic linking. In Fourth ACM Conference on Computer and Communications Security, pages 18–27, Zurich, Switzerland, April 1997. Association for Computing Machinery.
Darryl Dieckman, Perry Alexander, and Philip A. Wilsey. ActiveSPEC: A frame work for the specification and verification of active network services and secu rity policies. In Nevin Heintze and Jeannette Wing, editors, Workshop on Formal Methods and Security Protocols, Indianapolis, IN, June 1998. Informal proceedings available at http://www.cs.bell-labs.com/who/nch/fmsp/program.html.
Bruno Dutertre and Victoria Stavridou. Formal requirements analysis of an avion ics control system. IEEE Transactions on Software Engineering, 23(5):267–278, May 1997.
Steve Easterbrook, Robyn Lutz, Richard Covington, John Kelly, Yoko Ampo, and David Hamilton. Experiences using lightweight formal methods for requirements modeling. IEEE Transactions on Software Engineering, 24(1):4–14, January 1998.
Formal Methods Europe FME’ 97, volume 1313 of Lecture Notes in Computer Science, Graz, Austria, September 1997. Springer-Verlag.
Simon Fowler and Andy Wellings. Formal development of a real-time kernel. In Real Time Systems Symposium, pages 220–229, San Francisco, CA, December 1997. IEEE Computer Society.
Ganesh Gopalakrishnan and Phillip Windley, editors. Formal Methods in Computer-Aided Design (FMCAD’ 98), volume 1522 of Lecture Notes in Com puter Science, Palo Alto, CA, November 1998. Springer-Verlag.
David Greve. Symbolic simulation of the JEM1 microprocessor. In Phillip Windley, editors. Formal Methods in Computer-Aided Design (FMCAD’ 98), volume 1522 of Lecture Notes in Com puter Science, Palo Alto, CA, November 1998 Gopalakrishnan and Windley [17], pages 321–333.
David Hardin, Matthew Wilding, and David Greve. Transforming the theorem-prover into a digital design tool: From concept car to off-road vehicle. In Moshe Y. Vardi, editors. Computer-Aided Verification, CAV’ 98, volume 1427 of Lecture Notes in Computer Science, Vancouver, Canada, June 1998 Hu and Vardi [25], pages 39–44.
Klaus Havelund and N. Shankar. Experiments in theorem proving and model check ing for protocol verification. In Formal Methods Europe FME’ 96, volume 1051 of Lecture Notes in Computer Science, pages 662–681, Oxford, UK, March 1996. Springer-Verlag.
Mats P. E. Heimdahl and Barbara J. Czerny. Using PVS to analyze hierarchi cal state-based requirements for completeness and consistency. In IEEE High-Assurance Systems Engineering Workshop (HASE’ 96), pages 252–262, Niagara on the Lake, Canada, October 1996.
John Hoffman and Charlie Payne. A formal experience at Secure Computing Cor poration. In Moshe Y. Vardi, editors. Computer-Aided Verification, CAV’ 98, volume 1427 of Lecture Notes in Computer Science, Vancouver, Canada, June 1998 Hu and Vardi [25], pages 49–56.
Jozef Hooman. Compositional verification of real-time applications. In Willem Paul de Roever, Hans Langmaack, and Amir Pnueli, editors, Compositionality: The Sig nificant Difference (Revised lectures from International Symposium COMPOS’97), volume 1536 of Lecture Notes in Computer Science, pages 276–300, Bad Malente, Germany, September 1997. Springer-Verlag.
Ravi Hosabettu, Mandayam Srivas, and Ganesh Gopalakrishnan. Proof of correct ness of a processor with reorder buffer using the completion functions approach. In CAV’99 [8].
Alan J. Hu and Moshe Y. Vardi, editors. Computer-Aided Verification, CAV’ 98, volume 1427 of Lecture Notes in Computer Science, Vancouver, Canada, June 1998. Springer-Verlag.
Bart Jacobs, Joachim van den Berg, Marieke Huisman, Martijn van Berkum, Ulrich Hensel, and Hendrick Tews. Reasoning about Java classes. In Proceedings, ObjectO-riented Programming Systems, Languages and Applications (OOPSLA’ 98), pages 329–340, Vancouver, Canada, October 1998. Association for Computing Machinery. Proceedings issued as ACM SIGPLAN Notices Vol. 33, No. 10, October 1998.
Pertti Kellomäki. Verification of reactive systems using DisCo and PVS. In FME [15], pages 589–604.
Paul S. Miner and James F. Leathrum, Jr. Verification of IEEE compliant sub-tractive division algorithms. In Mandayam Srivas and Albert Camilleri, editors, Formal Methods in Computer-Aided Design (FMCAD’ 96), volume 1166 of Lec ture Notes in Computer Science, pages 64–78, Palo Alto, CA, November 1996. Springer-Verlag.
Abdel Mokkedem, Ravi Hosabettu, and Ganesh Gopalakrishnan. Formalization and proof of a solution to the PCI 2.1 bus transaction ordering problem. In Phillip Windley, editors. Formal Methods in Computer-Aided Design (FMCAD’ 98), volume 1522 of Lecture Notes in Com puter Science, Palo Alto, CA, November 1998 Gopalakrishnan and Windley [17], pages 237–254.
César Muñoz. PBS: Support for the B-method in PVS. Technical Report SRI-CSL 99-1, Computer Science Laboratory, SRI International, Menlo Park, CA, February 1999.
S. Owre, S. Rajan, J.M. Rushby, N. Shankar, and M.K. Srivas. PVS: Combining specification, proof checking, and model checking. In Thomas A. Henzinger, editors. Computer-Aided Verification, CAV’ 96, volume 1102 of Lecture Notes in Computer Science, New Brunswick, NJ, July/August 1996 Alur and Henzinger [3], pages 411–414.
Sam Owre, John Rushby, and N. Shankar. Integration in PVS: Tables, types, and model checking. In Ed Brinksma, editor, Tools and Algorithms for the Construction and Analysis of Systems (TACAS’ 97), volume 1217 of Lecture Notes in Computer Science, pages 366–383, Enschede, The Netherlands, April 1997. Springer-Verlag.
Sam Owre, John Rushby, Natarajan Shankar, and Friedrich von Henke. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107–125, February 1995.
Seungjoon Park and David L. Dill. Verification of cache coherence protocols by aggregation of distributed transactions. Theory of Computing Systems, 31(4):355–376, 1998.
N.S. Pendharkar and K. Gopinath. Formal verification of an O.S. submodule. In V. Arvind and R. Ramanujin, editors, 18th Conference on the Foundations of Software Technology and Theoretical Computer Science, volume 1530 of Lecture Notes in Computer Science, pages 197–208, Madras, India, December 1998. Springer-Verlag.
Holger Pfeifer, Detlef Schwier, and Friedrich W. von Henke. Formal verification for time-triggered clock synchronization. In Rushby [41], pages 193–212.
Amir Pnueli and Tamara Arons. Verification of data-insensitive circuits: An in order-retirement case study. In Phillip Windley, editors, Formal Methods in Computer-Aided Design (FMCAD’ 98), volume 1522 of Lecture Notes in Com puter Science, Palo Alto, CA, November 1998 Gopalakrishnan and Windley [17], pages 351–368.
S. P. Rajan, M. Fujita, K. Yuan, and M. T-C. Lee. ATM switch design by high level modeling, formal verification, and high level synthesis. ACM Transactions on Design Automation of Electronic Systems (TODAES), 3(4), October 1998.
John Rushby. PVS bibliography. Technical report, Computer Science Laboratory, SRI International, Menlo Park, CA. Constantly updated; available at http://www.csl.sri.com/pvs-bib.html.
John Rushby. Formal methods and their role in the certification of critical systems. In Roger Shaw, editor, Safety and Reliability of Software Based Systems (Twelfth Annual CSR Workshop), pages 1–42, Bruges, Belgium, September 1995. Springer.
John Rushby, editor. Dependable Computing for Critical Applications-7, Dependable Computing and Fault Tolerant Systems, San Jose, CA, January 1999. IEEE Computer Society. To appear (page numbers refer to preliminary proceedings).
John Rushby, Sam Owre, and N. Shankar. Subtypes for specifications: Predicate subtyping in PVS. IEEE Transactions on Software Engineering, 24(9):709–720, September 1998.
Hassen Saïdi and N. Shankar. Abstract and model check while you prove. In CAV’99 [8].
Jens U. Skakkebjk and N. Shankar. Towards a Duration Calculus proof assistant in PVS. In H. Langmaack, W.-P. de Roever, and J. Vytopil, editors, Formal Tech niques in Real-Time and Fault-Tolerant Systems, volume 863 of Lecture Notes in Computer Science, pages 660–679, Lübeck, Germany, September 1994. Springer Verlag.
David W. J. Stringer-Calvert. Mechanical Verification of Compiler Correctness. PhD thesis, University of York, Department of Computer Science, York, England, March 1998. Available at http://www.csl.sri.com/dave.sc/papers/thesis.html.
Kothanda Umamageswaran, Krishnan Subramani, Philip A. Wilsey, and Perry Alexander. Formal verification and empirical analysis of rollback relaxation. Jour nal of Systems Architecture (formerly published as Microprocessing and Micropro gramming: the Euromicro Journal), 44:473–495, 1998.
Ben L. Di Vito. A model of cooperative noninterference for integrated modular avionics. In Rushby [41], pages 251–268.
Friedrich von Henke, Stephan Pfab, Holger Pfeifer, and Harald Rueß. Case studies in meta-level theorem proving. In Jim Grundy and Malcolm Newey, editors, The orem Proving in Higher Order Logics: 11th International Conference, TPHOLs’ 98, volume 1479 of Lecture Notes in Computer Science, pages 461–478, Canberra, Australia, September 1998. Springer-Verlag.
M. Wahab. Verification and abstraction of flow-graph programs with pointers and computed jumps. Research Report CS-RR-354, Department of Computer Science, University of Warwick, Coventry, UK, November 1998. Available at http://www.dcs.warwick.ac.uk/pub/reports/rr/354.html.
Matthew M. Wilding, David S. Hardin, and David A. Greve. Invariant perfor mance: A statement of task isolation useful for embedded application integration. In Rushby [41], pages 269–282.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Owre, S., Rushby, J.M., Shankar, N., Stringer-Calvert, D.W.J. (1999). PVS: An Experience Report. In: Hutter, D., Stephan, W., Traverso, P., Ullmann, M. (eds) Applied Formal Methods — FM-Trends 98. FM-Trends 1998. Lecture Notes in Computer Science, vol 1641. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48257-1_24
Download citation
DOI: https://doi.org/10.1007/3-540-48257-1_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66462-8
Online ISBN: 978-3-540-48257-4
eBook Packages: Springer Book Archive