Skip to main content
SpringerLink
Log in

A comparison of PVS and Isabelle/HOL

  • Refereed Papers
  • Conference paper
  • First Online:
Book cover Theorem Proving in Higher Order Logics (TPHOLs 1998)

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

Included in the following conference series:

Abstract

There is an overwhelming number of different proof tools available and it is hard to find the right one for a particular application. Manuals usually concentrate on the strong points of a proof tool, but to make a good choice, one should also know (1) which are the weak points and (2) whether the proof tool is suited for the application in hand. This paper gives an initial impetus to a consumers' report on proof tools.

The powerful higher-order logic proof tools PVS and Isabelle are compared with respect to several aspects: logic, specification language, prover, soundness, proof manager, user interface (and more). The paper concludes with a list of criteria for judging proof tools, it is applied to both PVS and Isabelle.

Supported by the Netherlands Organisation for Scientific Research (NWO) under contract SION 612-316-125.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Sten Agerholm and Mike Gordon. Experiments with ZF set theory in HOL and Isabelle. In E. Thomas Schubert, Philip J. Windley, and James Alves-Foss, editors, Proceedings of the 8th International Workshop on Higher Order Logic Theorem Proving and Its Applications, Aspen Grove, UT, USA, volume 971 of LNCS. Springer-Verlag, September 1995.

    Google Scholar 

  2. Abdelwaheb Ayari and David A. Basin. Generic system support for deductive program development. In T. Margaria and B. Steffen, editors, Proceedings of the Workshop on Tools and Algorithms for the Construction and Analysis of Systems, Passau, Germany, volume 1055 of LNCS. Springer-Verlag, April 1996.

    Google Scholar 

  3. David Basin and Matt Kaufmann. The Boyer-Moore prover and Nuprl: An experimental compaxison. In Gérard Huet and Gordon Plotkin, editors, Logical Frameworks, pages 90–119. Cambridge University Press, 1991.

    Google Scholar 

  4. Victor A. Carreño and Paul S. Miner. Specification of the IEEE-854 floating-point standard in HOL and PVS. In HOL95: Eighth International Workshop on Higher-Order Logic Theorem Proving and Its Applications, Aspen Grove, UT, September 1995. Category B proceedings, available at http://lal.cs.byu.edu/lal/hol95/Bprocs/indexB.html.

    Google Scholar 

  5. Judith Crow and Ben L. Di Vito. Formalizing Space Shuttle software requirements. In First Workshop on Formal Methods in Software Practice (FMSP '96), pages 40–48, San Diego, CA, January 1996. Association for Computing Machinery.

    Google Scholar 

  6. Judy Crow, Sam Owre, John Rushby, Natarajan Shankar, and Mandayam Srivas. A tutorial introduction to PVS. Presented at WIFT '95: Workshop on Industrial-Strength Formal Specification Techniques, Boca Raton, Florida, April 1995. Available, with specification files, at http://www.csl.sri.com/wift-tutorial.html.

    Google Scholar 

  7. Database of existing mechanized reasoning systems. http://www-formal.stanford.edu/clt/ARS/systems.html.

    Google Scholar 

  8. Marco Devillers, David Griffioen, Judi Romijn, and Frits Vaandrager. Verification of a leader election protocol formal methods applied to IEEE 1394. Technical Report CSI-R9728, Computing Science Institute, Catholic University of Nijmegen, 1997.

    Google Scholar 

  9. Michael J.C. Gordon, Robin Milner, and Cristopher P. Wadsworth. Edinburgh LCF: A Mechanised Logic of Computation, volume 78 of LNCS. Springer-Verlag, 1979.

    Google Scholar 

  10. Mike Gordon. Notes on PVS from a HOL perspective. Available at http://www.cl.cam.ac.uk/users/mjcg/PVS.html, August 1995.

    Google Scholar 

  11. Elsa L. Gunter and Amy Felty, editors. Proceedings of the 10th International Workshop on Theorem Proving in Higher Order Logics, Murray Hill, NJ, USA, volume 1275 of LNCS. Springer-Verlag, August 1997.

    Google Scholar 

  12. Ulrich Hensel, Marieke Huisman, Bart Jacobs, and Hendrik Tews. Reasoning about classes in object-oriented languages: Logical models and tools. In Proceedings of ESOP at ETAPS '98, LNCS. Springer-Verlag, 1998. To appear.

    Google Scholar 

  13. Per Martin-Löf. Constructive mathematics and computer programming. In Sixth International Congress for Logic, Methodology, and Philosophy of Science, pages 153–175. North Holland, Amsterdam, 1982.

    Google Scholar 

  14. Nicholas A. Merriam and Michael D. Harrison. Evaluating the interfaces of three theorem proving assistants. In F. Bodart and J. Vanderdonckt, editors, Proceedings of the 3rd International Eurographics Workshop on Design, Specification, and Verification of Interactive Systems, Eurographics Series, Namur, Belgium, June 1996. Springer-Verlag.

    Google Scholar 

  15. Sam Owre. http://www.csl.sri.com/htbin/pvs/pvs-bug-list.

    Google Scholar 

  16. Lawrence C. Paulson. Isabelle: The next 700 theorem provers. In P. Odifreddi, editor, Logic and Computer Science, pages 361–386. Academic Press, 1990.

    Google Scholar 

  17. Lawrence C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of LNCS. Springer-Verlag, 1994.

    Google Scholar 

  18. Frank Pfenning. Isabelle bibliography. http://www.cl.cam.ac.uk/Research/HVG/Isabelle/biblio.html.

    Google Scholar 

  19. John Rushby. PVS bibliography, http://www.csl.sri.com/pvs-bib.html.

    Google Scholar 

  20. John Rushby, Sam Owre, and N. Shankar. Subtypes for specifications: Predicate subtyping in PVS. IEEE Transactions on Software Engineering, 24, 1998. To appear.

    Google Scholar 

  21. N. Shankar. PVS: Combining specification, proof checking, and model checking. In Mandayam Srivas and Albert Camilleri, editors, Formal Methods in Computer-Aided Design (FMCAD '96), volume 1166 of LNCS, pages 257–264, Palo Alto, CA, November 1996. Springer-Verlag.

    Google Scholar 

  22. Philip Wadler and Stephen Blott. How to make ad-hoc polymorphism less ad hoc. In 16'th ACM Symposium on Principles of Programming Languages, Austin, Texas, January 1989.

    Google Scholar 

  23. Markus Wenzel. Using axiomatic type classes in Isabelle, a tutorial, 1995. http://www4.Informatik.tu-muenchen.de/~wenzelm/papers.html.

    Google Scholar 

  24. Markus Wenzel. Type classes and overloading in higher-order logic. In Gunter and Felty [11].

    Google Scholar 

  25. William D. Young. Comparing verification systems: Interactive Consistency in ACL2. IEEE Transactions on Software Engineering, 23(4):214–223, April 1997.

    Article  Google Scholar 

  26. Vincent Zammit. A comparative study of Coq and HOL. In Gunter and Felty [11].

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. CWI, Amsterdam, The Netherlands

    David Griffioen

  2. Computing Science Institute, Univ. Nijmegen, PO Box 9010, 6500, GL Nijmegen, The Netherlands

    David Griffioen & Marieke Huisman

Authors
  1. David Griffioen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Marieke Huisman
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jim Grundy Malcolm Newey

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Griffioen, D., Huisman, M. (1998). A comparison of PVS and Isabelle/HOL. In: Grundy, J., Newey, M. (eds) Theorem Proving in Higher Order Logics. TPHOLs 1998. Lecture Notes in Computer Science, vol 1479. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0055133

Download citation

  • DOI: https://doi.org/10.1007/BFb0055133

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-64987-8

  • Online ISBN: 978-3-540-49801-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation