Systems Software Verification Summer School 2021
a hands-on introduction to automated verification and its application to distributed systems and protocols using the Ironâ‘ methodology.
The Systems Software Verification Summer School will be held from August 16 to August 27, 2021.
Follow the instructions in our README file to download and install the docker container with the pre-loaded tools you will need.
Please follow this step before the first lecture on Monday.
Day 1
Zoom recording, audio and chat
Slides:
Intro
Chapter 01 (Dafny mechanics)
Day 2
Zoom recording, audio and chat
Slides:
Chapter 01 (continued)
Chapter 02 (Specification)
Day 3
Zoom recording, audio and chat
Slides:
Chapter 01 and 02 Epilogue
Chapter 03 (State machines and behaviors)
Day 4
Zoom recording, audio and chat
Slides:
Review of Day 3 solutions
Chapter 04 (Proving properties)
Leader Election Invariant Discovery demo
Day 5
Zoom recording, audio and chat
Slides:
Chapter 05 (Modeling distributed and asynchronous systems)
Day 6
Zoom recording, audio and chat
Slides:
Chapter 5 recap
Midterm project (Distributed lock)
Day 7
Zoom recording, audio and chat
Slides:
Midterm review and Chapter 6 exercise preview
Chapter 6 (Refinement)
Day 8
Zoom recording, audio and chat
Slides:
Chapter 7 (Asynchronous specs)
Day 9
Zoom recording, audio and chat
Slides:
Chapter 8 (Application correspondence)
Chapter 9 (Multi-level refinement)
Day 10
Zoom recording, audio and chat
Slides:
Chapter 10 (Modules and automation)
Chapter 11 (Cross-host concurrency)
Chapter 12 (The future of systems verification)
- Manos Kapritsos (University of Michigan)
- Jon Howell (VMware Research)
- Rob Johnson (VMware Research)
- specify behavior with TLA+ state machines - verify protocols with Dafny automation
- debug a proof
- structure a proof with refinement
- manage proof automation challenges
- awareness of distributed or asynchronous systems
- no verification experience required
If you have questions, please contact
