Fault-Tolerant Distributed Theorem Proving.
In Harald Ganzinger, editor, Proceedings of the 16th International Conference on Automated Deduction, volume 1632 of Lecture Notes in Artificial Intelligence, pages 227–231, July 7–10 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.