Specification and Verification of Distributed Protocols
by Manos Kapritsos and Jon Howell
Fall 2024 edition, taught by Manos Kapritsos at the University of Michigan.
Please contact Manos (contact info here) if
you are looking for an earlier version of the course.
This course teaches a foundation of concepts that build up to the
ability to model a distributed, asynchronous protocol and prove it safe.
By the end of the course, participants will
- Be able to specify the desired behavior of real-world protocols using
refinement.
- Be able to articulate the guarantees provided by verification.
- Learn how to model protocols and prove them safe.
- Demonstrate mastery by building a distributed sharded key-value store and
proving that it always returns correct results.
Chapter 01: Dafny Basics
This chapter introduces the mathematical subset of Dafny needed to work the exercises in the rest of the course.Lectures
Exercises
Associated Libraries
Chapter 02: Specification
Specification is how we write down what a protocol does. A verification result is only as good as its specification.Lectures
Exercises
Chapter 03: State Machines
This chapter describes state machine models, a general tool we'll use to describe protocols and the environment they work in.Lectures
Exercises
Chapter 04: Invariants
Invariants are the central tool used to prove safety properties of protocols.Lectures
Exercises
Chapter 05: Distributed State Machines
Here we assemble state machines in an idiomatic way to represent a protocol and the environment the protocol operates in.Lectures
Exercises
Associated Libraries
Project 01: Distributed Lock Server
This midterm project demonstrates mastery of the concepts in chapters 1—5.Lectures
Exercises
- DistributedSystem
This file isn't editable because it's a trusted file that specifies how
hosts interact with one another over the network.
- Exercise 01: Midterm Project
Build a distributed lock server. Define how a host implements your
protocol in host.v.dfy; write your safety spec and proof here.
- Host protocol
Define the host state machine here: message type, state machine for executing one
host's part of the protocol.
- Network
This file isn't editable because it's a trusted file that specifies how
the network delivers packets, allowing reorder and duplicate delivery.
Associated Libraries
Chapter 06: Refinement
Refinement helps us write a specification that abstracts away the implementation details of the protocol.Lectures
Exercises
- Exercise 01: Event-based refinement
You are asked to provide the abstraction function and refinement proof
for a system describing the interactions among baristas and clients
when handing out, receiving and transfering bathroom keys.
Associated Libraries
Project 02: Sharded Key-Value Store
This final project demonstrates mastery of the concepts in chapters 1—6.Lectures
Exercises
Associated Libraries
Auxiliary Material:
Lectures
