A comparison of PVS and Isabelle/HOL

David Griffioen, Marieke Huisman

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

19 Citations (Scopus)

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.

Original languageEnglish
Title of host publicationTheorem Proving in Higher Order Logics
Subtitle of host publication11th International Conference, TPHOLs'98, Canberra, Australia, September 27 - October 1, 1998, Proceedings
EditorsJim Grundy, Malcolm Newey
Place of PublicationBerlin, Heidelberg
PublisherSpringer
Pages123-142
Number of pages20
ISBN (Electronic)978-3-540-49801-8
ISBN (Print)978-3-540-64987-8
DOIs
Publication statusPublished - 1998
Externally publishedYes
Event11th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 1998 - Canberra, Australia
Duration: 27 Sept 19981 Oct 1998

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume1479
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference11th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 1998
Country/TerritoryAustralia
CityCanberra
Period27/09/981/10/98

Keywords

  • n/a OA procedure

Fingerprint

Dive into the research topics of 'A comparison of PVS and Isabelle/HOL'. Together they form a unique fingerprint.

Cite this