Skip to main content
PRL Project

Proving Hybrid Protocols Correct

by Mark Bickford, Christoph Kreitz, Robbert van Renesse, Xiaoming Liu
2001

Proceedings of 14th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'01).

  • unofficial copies PDF, PS

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.

bibTex ref: BKVL01


cite link