Formally Verifying Hybrid Protocols
with the Nuprl Logical Programming Environment

Mark Bickford, Christoph Kreitz, Robbert van Renesse.

Technical Report, Cornell CS:2001-1839, Cornell University, Ithaca, NY, May 2001.


We describe a generic switching protocol for the construction of hybrid protocols and prove it correct with the Nuprl proof development system. We introduce the concept of meta-properties to characterize communication properties that can be preserved by switching and identify switching invariants that an implementation of the switching protocol must satisfy in order to work correctly.
Our work shows how a theorem prover with a rich specification language can contribute to the design and implementation of verifiably correct adaptive protocols and that it can have a large impact when being engaged at the earliest stages of the design.

This report was created automatically from formal Nuprl objects using Nuprl's formal documentation mechanism.

Back to overview of papers

Bibtex Entry

@TechReport{tr:Bickford+01b, author = "Mark Bickford and Christoph Kreitz and Robbert van Renesse", title = "Formally Verifying Hybrid Protocols with the Nuprl Logical Programming Environment", institution = "Cornell University. Department of Computer Science", number = "Cornell CS:2001-1839", year = "2001" }