Skip to main content
SpringerLink
Log in

PVS: An Experience Report

  • Conference paper
Applied Formal Methods — FM-Trends 98 (FM-Trends 1998)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1641))

Included in the following conference series:

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.

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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].

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

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

    Chapter  Google Scholar 

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

    Google Scholar 

  8. Computer-Aided Verification, CAV’ 99, Lecture Notes in Computer Science, Trento, Italy, July 1999. Springer-Verlag. To appear.

    Google Scholar 

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

    Chapter  Google Scholar 

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

    Article  Google Scholar 

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

    Google Scholar 

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

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

    Article  Google Scholar 

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

    Article  Google Scholar 

  15. Formal Methods Europe FME’ 97, volume 1313 of Lecture Notes in Computer Science, Graz, Austria, September 1997. Springer-Verlag.

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

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

    Chapter  Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

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

    Chapter  Google Scholar 

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

    Google Scholar 

  24. 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].

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  27. Pertti Kellomäki. Verification of reactive systems using DisCo and PVS. In FME [15], pages 589–604.

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

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

    Chapter  Google Scholar 

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

    Article  Google Scholar 

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

    Article  MATH  Google Scholar 

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

    Google Scholar 

  36. Holger Pfeifer, Detlef Schwier, and Friedrich W. von Henke. Formal verification for time-triggered clock synchronization. In Rushby [41], pages 193–212.

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

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

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

    Google Scholar 

  41. 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).

    Google Scholar 

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

    Article  Google Scholar 

  43. Hassen Saïdi and N. Shankar. Abstract and model check while you prove. In CAV’99 [8].

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  47. Ben L. Di Vito. A model of cooperative noninterference for integrated modular avionics. In Rushby [41], pages 251–268.

    Google Scholar 

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

    Chapter  Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science Laboratory, SRI International, Menlo Park, CA, 94025, USA

    S. Owre, J. M. Rushby, N. Shankar & D. W. J. Stringer-Calvert

Authors
  1. S. Owre
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. J. M. Rushby
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. N. Shankar
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. D. W. J. Stringer-Calvert
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. German Research Center for Artificial Intelligence (DFKI GmbH), Stuhlsatzenhausweg 3, D-66123, Saarbrücken, Germany

    Dieter Hutter  & Werner Stephan  & 

  2. Centro per la ricerca scientifica e tecnologica, ITC-irst, via Sommarive, 18, I-38050, Povo (Trento), Italy

    Paolo Traverso

  3. Bundesamt für Sicherheit in der Informationstechnik (BSI), Godesberger Allee 183, D-53175, Bonn, Germany

    Markus Ullmann

Rights and permissions

Reprints 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

Publish with us

Policies and ethics

Search

Navigation