Fault-Tolerant Distributed Theorem Proving

unofficial copies [PDF], [PS]

by Jason Hickey

Proceedings of 16th International Conference on Automated Deduction, H. Ganzinger (ed.), LNAI 1632, pp. 227-231, 1999.


In recent years, there have been many examples of significant formalization efforts in higher-order logics, including the formalization of Java, the verification of the SCI cache-coherency protocol, the verification of the AAMP5 avionics processor in PVS, the verification and automated optimization of Ensemble protocols, and many others. Higher-order logics are often chosen for these endeavors not only because they can formalize meta-principles, but also because they retain the conciseness and intuition of the original design.

While this model has been successful, it is expensive. We present an architecture, implemented in the MetaPRL logical framework, for distributing tactic proving over large groups of processors using the Ensemble group communication system. To counteract problems of reliability in distributed environments, we use Ensemble's fault recovery support. To preserve the large existing tactic base, we replace the existing tactic implementation with a functionally equivalent distributed tactic scheduler.