@inproceedings{ec0e46f74fef423ab333c21d0a28955e,
title = "A comparison of PVS and Isabelle/HOL",
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.",
keywords = "n/a OA procedure",
author = "David Griffioen and Marieke Huisman",
note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1998.; 11th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 1998 ; Conference date: 27-09-1998 Through 01-10-1998",
year = "1998",
doi = "10.1007/BFb0055133",
language = "English",
isbn = "978-3-540-64987-8",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "123--142",
editor = "Jim Grundy and Malcolm Newey",
booktitle = "Theorem Proving in Higher Order Logics",
address = "Germany",
}