Skip to main content


eCommons@Cornell >
College of Engineering >
Computer Science >
Computer Science Technical Reports >

Please use this identifier to cite or link to this item:
Title: Formally Verifying Hybrid Protocols with the Nuprl Logical ProgrammingEnvironment
Authors: Bickford, Mark
Kreitz, Christoph
van Renesse, Robbert
Keywords: computer science
technical report
Issue Date: 9-May-2001
Publisher: Cornell University
Abstract: 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.
Appears in Collections:Computer Science Technical Reports

Files in This Item:

File SizeFormat
2001-1839.ps751.34 kBPostscriptView/Open

Refworks Export

Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.


© 2014 Cornell University Library Contact Us