Proving Hybrid Protocols Correct
Mark Bickford, Christoph Kreitz, Robbert van Renesse, Xiaoming Liu.
In R. Boulton & P. Jackson, eds., 14th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2001), LNCS 2152, pp. 105-120, Springer Verlag, 2001.
Abstract
	We describe a generic switching protocol for the construction of hybrid protocols and prove it correct with the Nuprl proof development system. For this purpose we introduce the concept of meta-properties and use them to formally characterize communication properties that can be preserved by switching. We also identify switching invariants that an implementation of the switching protocol must satisfy in order to work correctly.

		Paper is available in postscript and pdf format		Slides of the conference presentation are available in compressed postscript and pdf format (Presentation: Mark Bickford)
Bibtex Entry
	@InProceedings{inp:Bickford+01c, author = "Mark Bickford and Christoph Kreitz and Robbert van Renesse and Xiaoming Liu", title = "Proving Hybrid Protocols Correct", booktitle = "14$^{th}$ International Conference on Theorem Proving in Higher Order Logics", year = "2001", editor = "Richard Boulton and Paul Jackson", volume = "2152", series = "Lecture Notes in Computer Science", pages = "105--120", publisher = "Springer Verlag" }