Protocol Proof Checking Simplified with SMT

We believe that recent advances in formal verification are on the verge of making formal verification a viable option for any protocol designer, assuming the designer understands the protocol well enough to explain why it works. We demonstrate this with an SMT-based proof checker developed at Intel...

Full description

Saved in:
Bibliographic Details
Main Authors: Tuttle, M. R., Goel, A.
Format: Conference Proceeding
Language:English
Subjects:
Arrays
Computational modeling
Computer crashes
consensus
Deductive Verification Framework (DVF)
distributed computing
Formal methods
model checking
Protocols
Reactive power
Satisfiability Modulo Theories (SMT)
Solid modeling
theorem proving
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:We believe that recent advances in formal verification are on the verge of making formal verification a viable option for any protocol designer, assuming the designer understands the protocol well enough to explain why it works. We demonstrate this with an SMT-based proof checker developed at Intel called the Deductive Verification Framework (DVF). We show how DVF can be used to prove correct a classical, fault-tolerant, distributed protocol for consensus, and describe how a protocol expert starting from scratch, with little-to-no prior familiarity with SMT or DVF, was able to model the protocol and prove it correct in six days and nine pages.
DOI:10.1109/NCA.2012.46