#Number
TR-PDS-1994-007

#Title
Causality for Time: How to Specify and Verify Distributed Algorithms

#Author
Vijay K. Garg
Alexander I. Tomlinson

#Abstract
We illustrate a technique for proving properties of
distributed programs.  Our technique avoids the notion of
global time or global state.  Furthermore, it does not require
any use of temporal logic.  All properties are proven using
induction on the happened-before relation and its
complement. We illustrate our technique by providing a formal
proof of Lamport's algorithm for mutual exclusion.

#Bib
@TechReport{,
  author = 	 "V.K. Garg and A.I. Tomlinson", 
  title = 	 "Causality for Time: How to Specify and 
		  Verify Distributed Algorithms" 
  institution =  "Parallel and Distributed Systems Laboratory, The
		  University of Texas at Austin", 
  year =	 1994,
  number =	 "TR-PDS-1994-007",
  note =	 "available via ftp or WWW at maple.ece.utexas.edu"
}