News
Currently, no news are available
Formal Verification of Systems Software
As society has become increasingly reliant on software, we need software to behave as expected, but it often does not. Even sophisticated testing practices leaves many potential behaviors untested, especially when the software encounters unlikely (or malicious) inputs and configurations. In this class, you will learn how to build robust software by writing code that is formally proven to be free of bugs with any input and any (valid) configuration: a much stronger guarantee than the one provided by traditional testing. The state-of-the-art tools and techniques you will learn in this course are used in leading academic research projects in Systems Verification, and in industry.
You will learn to describe a software systems’ behavior in a high-level specification language (derived from the Rust programming language) and to write an implementation that is mechanically verified to adhere to that high level specification using Verus, a Rust-based verification tool. Verus is a modern tool inspired by Dafny: it leverages SMT (satisfiability modulo theories) solvers to automatically handle the many of the trivial and not-so-trivial proof steps. At the end you will be able to design, implement, and prove correct a complex system, such as a distributed, sharded hash table.
A background in formal methods is helpful, but not required. The course will teach Rust and Verus syntax, and the formal verification principles we will use to write a systems' specification, and to prove the correctness of the implementation.
Course Structure (Weekly)
- 2-hour lecture
- 1-2 hour tutorial and exercise discussion
Course Development
The concept and part of this course (with exercises in Dafny, instead of Verus) have initially been developed by Manos Kapritsos, University of Michigan, Jon Howell, VMware Research, with later contributions by Tej Chajed, University of Wisconsin-Madison, and Andrea Lattuada (the instructor), MPI-SWS.