© 1995 by British Computer Society
| ||||||||||||||||||||||||||||||||||||||||||||||||||
Mechanical verification of distributed algorithms in higher-order logic*
Computer Science Department, University of California at Los Angeles, Los Angeles, CA 90024, USA Email: chou{at}cs.ucla.edu
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 HOL – an interactive proof assistant for higher-order logic develop 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.
* This paper is an expanded and fully revised version of [9]
Computer Science Department, University of California at Los Angeles, Los Angeles, CA 90024, USA Email: chou{at}cs.ucla.edu