MECHANICAL VERIFICATION OF DISTRIBUTED ALGORITHMS IN HIGHER-ORDER LOGIC

The only practical way to verify the correctness of distributed algorithms with a high degree of confidence is to construct machine-checked, formal correctness proofs. In this paper we explain how to do so using HOG-an interactive proof assistant for higher-order logic developed by Gordon and others. First, we describe how to build an infrastructure in HOL that supports reasoning about distributed algorithms, including formal theories of predicates, temporal logic, labeled transition systems, simulation of programs, translation of properties, and graphs. Then we demonstrate, via an example, how to use the powerful intuition about events and causality to guide and structure correctness proofs of distributed algorithms. The example used is the verification of PIF (propagation of information with feedback), which is a simple but typical distributed algorithm due to Segall.