Skip to main content
PRL Project

Proving Hybrid Protocols Correct

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

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

  • unofficial copies PDF, PS

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