#Number
TR-PDS-1994-008

#Title
Using Induction to Prove Properties of Distributed Programs

#Author
Vijay K. Garg
Alexander I. Tomlinson

#Abstract
Proofs of distributed programs are often informal due to the
difficulty of developing formal proofs.  Properties of
distributed programs are often stated using Lamport's
causally-precedes relation and its complement,
not-causally-precedes.  Properties that involve the
causally-precedes relation are fairly straight forward to
prove using induction.  However, properties that involve
not-causally-precedes are quite difficult to prove.  Such
properties are common since predicates on the global state of
a system implicitly use the not-causally-precedes relation.
This paper presents a method of induction on the
not-causally-precedes relation and demonstrates the technique
by formally proving a variant of the well known algorithm for
maintaining a vector clock.

#Bib
@InProceedings{,
  author = 	 "A.I. Tomlinson and V.K.Garg",
  title = 	 "Using Induction to Prove Properties of 
		 Distributed Programs",
  pages =	 "478--485",
  booktitle =	 "Proc. of the 5th IEEE Symposium on Parallel and
		  Distributed Processing",
  year =	 1993,
  organization = "IEEE",
  address =	 "Dallas, TX",
  month = 	 "December",
  note =	 "available via ftp or WWW at maple.ece.utexas.edu
		  as technical report TR-PDS-1994-008"
}