Verifying Distributed Protocols Using a Logic of Events

Robert L. Constable
Cornell University
March 2004

Abstract

This talks presents a new logical language for specifying and reasoning about
distributed algorithms. It is based on our direct formalization of the
foundational ideas of Leslie Lamport that we call a Logic of Events. Mark
Bickford and I have undertaken this formulation, and Mark has implemented the
theory in Cornell's Nuprl proof development system. He has mechanically
verified interesting protocols such as leader election in various graph
structures. We are also applying these methods to verifying patterns in the
BBN UAV distributed system.