Systems Software Verification Summer School 2020

a hands-on introduction to automated verification and its application to distributed systems protocols using the Ironâ­‘ methodology.

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 (Recording starts a few minutes late, please see the slides for the content up to that time)
Slides:
Intro
Chapter 01
Chapter 02

Day 2
Zoom recording, audio and chat
Slides:
Chapter 03
Chapter 04

Day 3
Zoom recording, audio and chat
Slides:
Chapter 05
Midterm project
Chapter 07

Day 4
Zoom recording, audio and chat
Slides:
Final project
Chapter 09
Chapter 10
Chapter 11

Day 5
Zoom recording, audio and chat
Slides:
Chapter 12
Chapter 13

Organizers:
  • Manos Kapritsos (University of Michigan)
  • Jon Howell (VMware Research)
  • Rob Johnson (VMware Research)
Syllabus includes:
  • specify behavior with TLA+ state machines - verify protocols with Dafny automation
  • debug a proof
  • structure a proof with refinement
  • manage proof automation challenges
Prerequisites:
  • awareness of distributed or asynchronous systems
  • no verification experience required

The Systems Software Verification Summer School was held from July 13 to July 17, 2020.



If you have questions, please contact