Abstract
In recent years, there have been many examples of signicant formalization ef- forts in higher-order logics, including the formalization of Java [12], the veri cation of the SCI cache-coherency protocol [5], the verication of the AAMP5 avionics processor [11] in PVS [2], the verication and automated optimization of Ensemble protocols [10,7], and many others. Higher-order logics are often cho- sen for these endeavors not only because they can formalize meta-principles, but also because they retain the conciseness and intuition of the original design.
This is a preview of subscription content, log in via an institution to check access.
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
Maria Paola Bonacina and William McCune. Distributed theorem proving by peers. In 1194 Conference on Automated Deduction (CADE12), pages 841–845, 1994.
Judy Crow, Sam Owre, John Rushby, Natarajan Shankar, and Man-dayam Srivas. A Tutorial Introduction to PVS. In WIFT’ 95: Workshop on Industrial-Strength Formal Specification Techniques, April 1995. http://www.csl.sri.com/sri-csl-fm.html.
J. Denzinger and Dirk Fuchs. Cooperation in theorem proving by loosely coupled heuristics. Technical Report SR-97-04, University of Kaiserslautern, 1997.
R.L. Constable et.al. ImplementingMathematics in the NuPRL Proof Development System. Prentice-Hall, 1986.
A. Felty, D. Howe, and F. Stomp. Protocol verification in Nuprl. In CAV’98, Lecture Notes on Computer Science. Springer, 1998.
Mark Hayden. The Ensemble system. Technical Report TR98-1662, Cornell University, 1998.
Jason Hickey, Nancy Lynch, and Robbert van Renesse. Specifications and proofs for Ensemble layers. In TACAS’ 99, March 1999.
Jason J. Hickey. Nuprl-Light: An implementation framework for higher-order logics. In 14th International Conference on Automated Deduction. Springer, 1997.
Paul Bernard Jackson. Enhancing the NuPRL Proof Development System and Applying it to Computational Abstract Algebra. PhD thesis, Cornell University, January 1995.
Christoph Kreitz, Mark Hayden, and Jason Hickey. A proof environment for the development of group communications systems. In 15th International Conference on Automated Deduction, pages 317–332. Springer, 1998.
Steven P. Miller and Mandayam Srivas. Formal verification of the AAMP5 microprocessor: A case study in the industrial use of formal methods. In WIFT’ 95: Workshop on Industrial-Strength Formal Specification Techniques, pages 2–16, Boca Raton, FL, 1995.
Tobias Nipkow and David von Oheimb. Javalight is type-safe definitely. In Proc. 25th ACM Symp. Principles of Programming Languages, pages p. 161–170. ACM Press, New York, 1998.
Didier Rémy and Jérôme Vouillon. Objective ML: A simple object-oriented extension of ML. In ACM Symposium on Principles of Programming Languages, pages 40–53, 1997.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hickey, J. (1999). Fault-Tolerant Distributed Theorem Proving. In: Automated Deduction — CADE-16. CADE 1999. Lecture Notes in Computer Science(), vol 1632. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48660-7_19
Download citation
DOI: https://doi.org/10.1007/3-540-48660-7_19
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66222-8
Online ISBN: 978-3-540-48660-2
eBook Packages: Springer Book Archive