#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"
}