News
Chapter 1 exercises due on Friday evening. Please reach out directly if there are issues.Written on 18.11.24 by Andrea Lattuada Dear Students, This is a gentle reminder that the Chapter 01 exercises are due on Friday November 22nd at 23:59. A few notes and reminders:
Dear Students, This is a gentle reminder that the Chapter 01 exercises are due on Friday November 22nd at 23:59. A few notes and reminders:
See you on Wednesday in E1 5 029. |
Lecture on November 8th canceled. First set of graded exercises will be released on Friday.Written on 07.11.24 by Andrea Lattuada Dear Students, I am currently traveling for a conference and due to a flight delay I will not be able to make it back to Saarbrücken by Friday morning, so the in-person lecture is canceled this week. We will nonetheless release the first set of graded exercises on Friday, and you will have two weeks… Read more Dear Students, I am currently traveling for a conference and due to a flight delay I will not be able to make it back to Saarbrücken by Friday morning, so the in-person lecture is canceled this week. We will nonetheless release the first set of graded exercises on Friday, and you will have two weeks to complete them. I have already covered the lecture material necessary to complete these exercises but I will record and publish a brief introduction to the exercises with a refresher and some hints. You will also be able to ask questions at the tutorial next week. See you on Wednesday! |
Tutorial on October 30th will take place in E1 5 002. No lecture on Friday, no tutorial next week.Written on 30.10.24 by Andrea Lattuada The tutorial today (October 30th) will take place in E1 5 002, the same room as the first two lectures, at 16:10. This is for this week only. We'll move to E1 5 029 for both lectures and tutorials starting next week. Also note that there (obviously) won't be a lecture this Friday (November 1st),… Read more The tutorial today (October 30th) will take place in E1 5 002, the same room as the first two lectures, at 16:10. This is for this week only. We'll move to E1 5 029 for both lectures and tutorials starting next week. Also note that there (obviously) won't be a lecture this Friday (November 1st), and there won't be a tutorial next week (on Wednesday November 6th). After today's tutorial, the next session will be the lecture on Friday November 8th at 10:15 in E1 5 029. |
Let us know which hardware/software configuration you're running by Monday 28th.Written on 25.10.24 (last change on 25.10.24) by Andrea Lattuada At the tutorial next week we will provide instructions to set up Verus. To make sure that we can support your hardware/software configuration, please fill in the two polls on discourse here: https://sysverification.sic.saarland/t/what-configuration-are-you-running/ by the evening of Monday 28th (October 2024). |
Tutorials will be on Wednesdays at 16:10 (till 17:00). First tutorial on Wednesday October 30th.Written on 22.10.24 (last change on 22.10.24) by Andrea Lattuada Dear all, based on the preferences you entered, we've scheduled the tutorial on Wednesdays at 16:10-17:00. The first tutorial will be next week, on October 30th. As a reminder, the tutorials will be recorded, but we strongly recommend in-person attendance, as they will be interactive and give you the… Read more Dear all, based on the preferences you entered, we've scheduled the tutorial on Wednesdays at 16:10-17:00. The first tutorial will be next week, on October 30th. As a reminder, the tutorials will be recorded, but we strongly recommend in-person attendance, as they will be interactive and give you the opportunity to ask questions about the material, take home exercises, and projects. Thank you all for entering your preferences. |
The lectures and tutorials for this course will be recorded, but we recommend attending in person,
as the lectures and tutorials are designed to be interactive.
You will submit graded exercises and projects online, no attendance is needed to submit these.
➡️ Lecture Recordings, Slides, and other material
➡️ Setting up Verus, documentation, and how to submit take-home exercises
Systems Software underpins our modern computing infrastructure, both in datacenters, and on personal devices. When it fails or misbehaves because of bugs, they can lose or leak your data, make online services unavailable for a long period of time, and -- if you are a developer -- cost your company its reputation and revenue. For example, a corruption in a filesystem, or storage system may make you lose your e-mail, messages, photos, or banking information.
Regular testing can be insufficient for complex (often distributed) systems, which is why you keep hearing about software failures in online services. In this course, you will learn how to formally verify the correctness of these programs, so that we can have near certainty that the software we deploy is bug-free. You will learn how to model the expected behavior of a system, -- for example, how a distributed storage system (like Amazon's S3) is nothing else than a very simple map from keys to values from the perspective of its clients. You will then learn how to write Rust code for and such a system and formally prove, at compile time, that this implementation matches the simple key-value abstract model, i.e. that the program code is correct, without however having to run it or any tests.
We'll use the Rust-based Verus verification framework. Verus is being developed primarily at MPI-SWS, CMU, Microsoft, and is used for cutting edge research at MPI-SWS, MIT, CMU, UIUC (and more), and in industry: for example, Microsoft is developing a storage system verified with Verus, and Amazon is evaluating Verus to verify some of their systems. On the Verus website you can find a list of research papers and projects using Verus.
You will learn the necessary 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. Verus is a modern semi-automated tool that leverages SMT (satisfiability modulo theories) solvers to automatically handle many of the trivial and not-so-trivial steps of the proofs: you will learn how to write the rest of the proof as assertions written in Rust. At the end you will be able to design, implement, and prove correct a small but complex system, such as a distributed, sharded hash table.
Prerequisites. Programming experience, preferably in a Systems language (like C/C++). Knowing Rust is not a prerequisite. A background in formal methods and/or logic is helpful, but not required.
Course Structure (Weekly)
- 1.5-hour lecture: Fridays 10:15-11:45 in E1 5 029
More info on how to find the rooms. - 1 hour tutorial and exercise discussion: Wednesdays 16:10-17:00 in E1 5 029 (starting October 30th)
- take home exercises (graded)
Evaluation
- need to pass 7 out of 8 of take home exercise chapters to register for the exam
- students get feedback on submissions, and can resubmit take home exercises
- note that "Chapter 00: Submitting" is not part of the graded take home exercises and was simply a test of the ability of Student to submit through CMS
- 2 graded projects, done individually (25% + 25%)
- need to pass (50% score) both project to register for the exam
- exam (50%) (with a re-exam)
- you will need to pass 7 out of 8 of the take home exercises, and score at least 50% in both projects to register for the exam (and re-exam)
Exam Dates
- End of Term: February 26, 9:30-12:00 in E1 3 hall 002.
- Re-Exam: March 18th, 9:30-12:00 in E1 3 hall 002.
(The actual duration may be a bit shorter than the full 2.5 hours slots.)
Projects
- (mid-term) design and verify a distributed lock service
- (final, in parallel to lectures on advanced topics) design and verify a sharded key-value store
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.
Schedule (tentative)
- 2024-10-18: Intro
- 2024-10-25: Verus Mechanics (datatypes, predicates, assertions)
- 2024-11-08: Specification and state machines
- 2024-11-15: State machines and behaviors
- 2024-11-22: Proving properties and inductive invariants
- 2024-11-29: Leader election demo
- 2024-12-06: Modeling distributed and asynchronous systems
- 2024-12-13: Project 1 assignment
- 2024-12-20: Recap
- 2025-01-10: Asynchronous specifications
- 2025-01-17: Application correspondence
- 2025-01-24: Multi-layer refinement
- 2025-01-31: Cross-host concurrency + Project 2 assignment
- 2025-02-07: Case studies + Research
Take-home exercises and project rules
- Exercises and projects are individual
- Okay to clarify problem or discuss Verus syntax
- on Discourse, in person
- It is not okay to discuss solutions
- Do not publish your exercise solutions anywhere
- You may not use /* */ comments
- You must leave the existing /* */ comments in place
- You may only change text between /*{*/ and /*}*/
- You are not allowed to add axioms (I have not taught you how to do this)
- You are not allowed to use assume(_); or admit(); in the code you submit
- Do not rename the files
Verus logo CC-BY Verus Contributors, Rust logo CC-BY Rust Foundation