News

No tutorial this week; please register for office hours

Written on 20.01.25 (last change on 20.01.25) by Andrea Lattuada

Dear Students, there will not be a tutorial on Wednesday (January 22nd) this week.

If you need help with the project, I will be offering office hours sessions between the end of this week and beginning of next week. Please register your interest in the "Registration" that I opened ("Project 02 -… Read more

Dear Students, there will not be a tutorial on Wednesday (January 22nd) this week.

If you need help with the project, I will be offering office hours sessions between the end of this week and beginning of next week. Please register your interest in the "Registration" that I opened ("Project 02 - Office Hours - 01").

Exercise chapter 6 due soon

Written on 17.01.25 by Andrea Lattuada

Dear Students, don't forget that you need to pass 7 out of 8 chapters of exercises to be admitted to the exam, and note that Chapter 6 is due soon, on January 21st. If you haven't started on it, note that solving exercise01 is sufficient to pass, which should be fairly straightforward. I recommend not… Read more

Dear Students, don't forget that you need to pass 7 out of 8 chapters of exercises to be admitted to the exam, and note that Chapter 6 is due soon, on January 21st. If you haven't started on it, note that solving exercise01 is sufficient to pass, which should be fairly straightforward. I recommend not waiting till the last day to submit, as usual, in case there are issues with your submission.

Chapter 07 released tomorrow, due on January 28th

Written on 15.01.25 by Andrea Lattuada

Dear Students, as mentioned in class, tomorrow we will release the handout for Chapter 07. The submission is due on January 28th.
A few notes:

  • Like for chapter 5, submitting a compliant file (even if it doesn’t verify) grants you a point
  • If you pass the auto-grader (no hidden checks, just… Read more

Dear Students, as mentioned in class, tomorrow we will release the handout for Chapter 07. The submission is due on January 28th.
A few notes:

  • Like for chapter 5, submitting a compliant file (even if it doesn’t verify) grants you a point
  • If you pass the auto-grader (no hidden checks, just compliance and successful verification), you get an additional point
  • You need 1 out of 2 points needed to pass
    • I still strongly recommend attempting the exercise, as there may be questions about the refinement to an implementation in the exam
    • but you should prioritize Project 2.
  • If you score 2 points, you get a 8% bonus on the overall score of the projects + exam
    (relative to the maximum 100% score, not your score)
    ​​​​​This does not affect or change the requirement to pass the exercises and projects to be admitted to the exam
  • I reserve the right to add additional constraints and invalidate the bonus if a solution trivializes the verification in a way that I did not guard against (i.e. you should be faithful to the intent of the exercise -- if you are, then you'll likely get the bonus if you get the exercise to verify successfully)

Compatibility with older glibc (ie older Linux distros)

Written on 13.01.25 by Andrea Lattuada

Dear Students, it came to my knowledge that the new version of Verus that was published last week did not work with older versions of glibc (ie a number of slightly older Linux distributions were affected). I published a new version that should restore the same level of support as before. If you’re on… Read more

Dear Students, it came to my knowledge that the new version of Verus that was published last week did not work with older versions of glibc (ie a number of slightly older Linux distributions were affected). I published a new version that should restore the same level of support as before. If you’re on Linux, and you have had issues with the new Verus version, you can download the new version (from the Verus setup page on CMS). If the version you’re using works for you, you don’t need to do anything. There should be no change in which code verifies between the two versions. My apologies for the inconvenience if you were affected.

Project 1 Office Hours Registration

Written on 08.01.25 (last change on 08.01.25) by Andrea Lattuada

Dear Students, if you want to discuss Project 1 in an office-hours setting, please register for it using the "Registration" in CMS that I just opened (and that remains open until tomorrow evening). Based on registrations there I will schedule office-hours meetings on Friday January 10th and Monday… Read more

Dear Students, if you want to discuss Project 1 in an office-hours setting, please register for it using the "Registration" in CMS that I just opened (and that remains open until tomorrow evening). Based on registrations there I will schedule office-hours meetings on Friday January 10th and Monday January 13th.

Clarification on the English-language description of Project 01

Written on 07.01.25 by Andrea Lattuada

Dear all, I would like to make a small clarification to the English-language description in the handout of Project 1.
Specifically, you should read the fourth paragraph as follows (it is unchanged, except for the part added in bold):

To guard against duplicate messages, the nodes associate a… Read more

Dear all, I would like to make a small clarification to the English-language description in the handout of Project 1.
Specifically, you should read the fourth paragraph as follows (it is unchanged, except for the part added in bold):

To guard against duplicate messages, the nodes associate a monotonically increasing epoch number with the lock. Initially, node 0 (if present) holds the lock and its epoch number is 1, while all other nodes with an epoch of 0 (and not holding the lock). A node that holds the lock can “grant” it to another node by sending them a “Grant” message which has an epoch number that is greater than the node's epoch number. A node that receives such a message will become the new holder and will set its epoch number to the message’s epoch number. A node should reject (i.e. not receive) lock "Grant" messages with epochs lower or equal to their current epoch, as these are stale (duplicates).

---

Additionally, please note that I believe it is very unlikely that a safety property that is expressed concisely will also be inductive by itself for this protocol. If you did not need any additional conjuncts in your `inv` in addition to `safe` I would strongly recommend carefully inspecting your protocol definition and safety property.

All of this will also be discussed during the tutorial tomorrow.

Homework Virtual Office Hours Today

Written on 07.01.25 by Andrea Lattuada

Dear Students, if you need help with one of the exercises, or have questions regarding the project, please send me an email (andrea@mpi-sws.org) to book a time between 11:00 and 16:30 today. I will acknowledge the time (if available, or suggest a different time) and then we will meet in this Zoom… Read more

Dear Students, if you need help with one of the exercises, or have questions regarding the project, please send me an email (andrea@mpi-sws.org) to book a time between 11:00 and 16:30 today. I will acknowledge the time (if available, or suggest a different time) and then we will meet in this Zoom room:

https://eu02web.zoom-x.de/j/61362418777?pwd=L6hG2gnXZIyaiZbuE26MKQEbnrOhL9.1
Meeting ID: 613 6241 8777
Passcode: 581423

If you've already sent me an email, you will get a response in the next hour or so.

Please also let me know if you need help but today does not work for you.

Chapter 4, exercise 1 and 3 individual feedback available

Written on 01.01.25 (last change on 08.01.25) by Andrea Lattuada

Dear Students, just a quick note that I have made available the individual feedback for Chapter 4 for students that submitted by December 20th. Please make sure to download it by Friday January 3rd, as I will start running the auto-grader again on Saturday January 4th, which (due to a limitation in… Read more

Dear Students, just a quick note that I have made available the individual feedback for Chapter 4 for students that submitted by December 20th. Please make sure to download it by Friday January 3rd, as I will start running the auto-grader again on Saturday January 4th, which (due to a limitation in how the feedback is uploaded and updated) will overwrite the manual feedback. If you are unable to download the feedback by then, you will be able to request it directly via mail from me afterwards.

Chapter 3, exercise 3 feedback published

Written on 29.12.24 (last change on 08.01.25) by Andrea Lattuada

Dear all, just a quick note that I have updated the chapter 3 feedback with individual feedback for exercise 3, in addition to exercise 2. I recommend having a look, as it may be helpful for the project. Please send me an email if you have any questions.

Project 1 Patch

Written on 29.12.24 (last change on 08.01.25) by Andrea Lattuada

Dear Students, apologies for a second email in one day.

The first few submissions for project 01 have made me notice that, while the project file is correct, it allows for certain kinds of unfortunate typos that may make your proof meaningless. I cannot guard against the majority of them, obviously… Read more

Dear Students, apologies for a second email in one day.

The first few submissions for project 01 have made me notice that, while the project file is correct, it allows for certain kinds of unfortunate typos that may make your proof meaningless. I cannot guard against the majority of them, obviously (you are in charge of being careful in writing your specification and safety property, as we discussed at length), but in an attempt to better evaluate your skills in the project I have added a pseudo_liveness proof obligation (akin to the ones you have seen before in exercises) for exercise01.rs that will hopefully help you catch certain careless mistakes.

If you have already submitted, I have applied the patch to your code and re-submitted for you: you can download the updated code from your personal status page. If you have not submitted you have two options:

(a) recommended, especially if you've only done a little bit of work: re-download the handout and copy over your solution within the grading markers,

(b) use the write up at https://cms.sic.saarland/sysverification2425/contents/view/6 to apply the change to exercise01.rs (note that you will need to do this carefully, to make sure that your code will pass the auto-grader check for changes outside the grading markers)

Sorry for the inconvenience, and hope this helps.

Project 01 clarification (only change code within the /*{*/ and /*}*/ markers!)

Written on 29.12.24 (last change on 08.01.25) by Andrea Lattuada

Dear Students, one quick clarification. As for all the other exercises you are still only allowed to change code within the /*{*/ and /*}*/ markers. To let you check that your code is compliant, contrary to what I had mentioned before, I will be running the auto-grader on the project periodically, so… Read more

Dear Students, one quick clarification. As for all the other exercises you are still only allowed to change code within the /*{*/ and /*}*/ markers. To let you check that your code is compliant, contrary to what I had mentioned before, I will be running the auto-grader on the project periodically, so you can get reports in case you accidentally make changes outside the markers. One more reason to submit early, even partial progress.

Score for chapter 5

Written on 27.12.24 (last change on 08.01.25) by Andrea Lattuada

Dear Students, a quick heads up on how chapter 5 is scored (due to its unusual requirement that the minimum score to pass is 0/1 as long as you do submit `extercise04.rs` to the Chapter 04, 05 submission): in the Tests/Exam view for Chapter 5 you will see that you will receive 1 point if you have… Read more

Dear Students, a quick heads up on how chapter 5 is scored (due to its unusual requirement that the minimum score to pass is 0/1 as long as you do submit `extercise04.rs` to the Chapter 04, 05 submission): in the Tests/Exam view for Chapter 5 you will see that you will receive 1 point if you have submitted `exercise04.rs`, and 2 points if it passes the auto-grader: I have set the pass score on CMS to 1/2 points, which you will get if you have at least submitted `exercise04.rs`. During the non-teaching period I will only update the scores occasionally, so if you have recently submitted chapter 5, it may be that the point(s) have not been awarded yet. Let me know if something is unclear, or if you have any questions.

Project 01 Released. Deadline 14.01.2025, 23:59.

Written on 26.12.24 (last change on 08.01.25) by Andrea Lattuada

Dear Students, I have released the handout for the distributed lock server project. The project is due at 23:59 on Tuesday 14.01.2025. I will not be running the auto-grader on the project, as there is no automatic feedback in addition to successful verification. Read the handout carefully, and refer… Read more

Dear Students, I have released the handout for the distributed lock server project. The project is due at 23:59 on Tuesday 14.01.2025. I will not be running the auto-grader on the project, as there is no automatic feedback in addition to successful verification. Read the handout carefully, and refer to the last part of the lecture of December 20th: both contain information on what is expected of you for the project, and how it will be graded (remember that a passing score is required for admission to the exam, and the score for this project will account for 25% of how your performance in the course will be graded).

The project will be scored according to the following criteria:

  • Adherence to the English-language specification of the state, steps, and safety property;
  • Understandability of the state machine state and steps (prefer enum/structs; use comments where necessary, but not in excess!);
  • Identification of inductive invariants, and completeness of the safety proof.

You will not get a passing score for the project if you just submit the handout file unchanged (even if it verifies). You will get a higher score if you submit a project that does not verify but has correct, well-written transitions, an accurate and concise safety property, and at least an attempt to identify the inductive invariant and to write the safety proof. A proof that works for only some of the cases (e.g. some of the host steps) is better than an empty proof, or no invariant.

If you have any questions please reach out. As you work through the project, I strongly recommend you frequently submit your partial work, as that will allow me to give guidance or spot potential common misunderstanding earlier rather than later. I will only evaluate the last submission.

Chapter 5 handout released, and Chapter 5 information

Written on 22.12.24 (last change on 08.01.25) by Andrea Lattuada

Dear Students, I have released the handout for chapter 5, which consists of a single file, exercise04.rs, that you can add to the files for chapter 4. Note that it verifies successfully with the trivial definition of safety for the protocol included in the handout for exercise03.rs: this is a… Read more

Dear Students, I have released the handout for chapter 5, which consists of a single file, exercise04.rs, that you can add to the files for chapter 4. Note that it verifies successfully with the trivial definition of safety for the protocol included in the handout for exercise03.rs: this is a meaningless proof, as it is a proof that true is a valid safety property for two-phase commit. Only work on this exercise once you believe you have a sufficiently accurate specification of two-phase commit in exercise03.rs. The passing score for this Chapter 5 is 0/1, assuming you make an attempt and submit: submitting exercise04.rs alongside the Chapter 4 files to the "Chapter 4, Chapter 5" submission is sufficient to pass Chapter 5. The passing score for Chapter 4 remains 2/3 (for exercise01, exercise02, exercise03). While it's not required to pass, I recommend you work on trying to complete the proof, as it's good practice for the project, which will be released soon.

Chapter 3, exercise 2 feedback published

Written on 20.12.24 (last change on 08.01.25) by Andrea Lattuada

Dear all, just a quick note that I have updated the chapter 3 feedback with individual feedback for exercise 2. Individual feedback for chapter 3, exercise 3 will be published in the next couple of days. Please send me an email if you have any questions.

Chapter 4 Patch

Written on 18.12.24 (last change on 08.01.25) by Andrea Lattuada

Dear Students, there is a small issue in exercise01.rs in the handout I distributed for Chapter 4 (and Chapter 5). For an accurate model of the system, we need to state that the network's sent_msgs Set is finite as a well_formed condition. This will not have prevented you from proving safety and is a… Read more

Dear Students, there is a small issue in exercise01.rs in the handout I distributed for Chapter 4 (and Chapter 5). For an accurate model of the system, we need to state that the network's sent_msgs Set is finite as a well_formed condition. This will not have prevented you from proving safety and is a weaker network property (so it's not incorrect, just models a network where the messages could be infinite); but the update is still a valid, and more accurate, network model and makes the proof for Chapter 5 simpler.

If you have already submitted, I have applied the patch to your code and re-submitted for you: you can download the updated code from your personal status page. If you have not submitted you have two options:

(a) recommended, especially if you've only done a little bit of work: re-download the handout and copy over your solution within the grading markers,

(b) use the write up at https://cms.sic.saarland/sysverification2425/5/Chapter_4_Patch to apply the change to exercise01.rs (note that you will need to do this carefully, to make sure that your code will pass the auto-grader check for changes outside the grading markers)

Sorry for the inconvenience.

I will also soon update the incremental.rs example from the last lecture demos to match the same network model.

Chapter 4 Handout Released

Written on 14.12.24 (last change on 08.01.25) by Andrea Lattuada

Dear Students, the handout for chapter 4 has been released. It includes exercise01.rs, exercise02.rs, and exercise03.rs.
You can submit your solution to the Chapter 04, Chapter 05 submission on CMS. We will later release chapter 5, which consists of exercise04.rs. When we do, you can add… Read more

Dear Students, the handout for chapter 4 has been released. It includes exercise01.rs, exercise02.rs, and exercise03.rs.
You can submit your solution to the Chapter 04, Chapter 05 submission on CMS. We will later release chapter 5, which consists of exercise04.rs. When we do, you can add exercise04.rs alongside the files in this handout (it depends on them), and then resubmit to the Chapter 04, Chapter 05 submission on CMS.

You need 2/3 points to pass Chapter 4. We'll communicate the pass threshold for Chapter 5 when we release it.

While the deadline for both Chapter 4 and Chapter 5 is January 7th 2025, as noted in the lecture: if you submit your solution to Chapter 4 by the end-of-day on December 20th I will give you feedback on it. This feedback can be quite useful for the first graded project, which will be released on December 21st.
 

Office Hours Wednesday December 11 from 9:00 till 14:00

Written on 10.12.24 (last change on 08.01.25) by Andrea Lattuada

Dear Students, tomorrow I will be holding a virtual office hours session for the Chapter 3 exercises from 9:00 till 14:00.

You can either walk into my office in E1 5 (SWS) 448, or join the following Zoom meeting:
https://eu02web.zoom-x.de/j/67226483076?pwd=bkto7auPFHecO5uCXUmp9aCHJTzkaQ.1
Meeting… Read more

Dear Students, tomorrow I will be holding a virtual office hours session for the Chapter 3 exercises from 9:00 till 14:00.

You can either walk into my office in E1 5 (SWS) 448, or join the following Zoom meeting:
https://eu02web.zoom-x.de/j/67226483076?pwd=bkto7auPFHecO5uCXUmp9aCHJTzkaQ.1
Meeting ID: 672 2648 3076
Passcode: 000725

There may be a wait, if multiple people join the Zoom meeting or show up at the same time. My apologies in advance.

If you need help and cannot make it to the office hours tomorrow, please email me: andrea@mpi-sws.org

Chapter 2 deadline extended to Wednesday December 4th

Written on 02.12.24 (last change on 08.01.25) by Andrea Lattuada

Dear Students, due to the (albeit brief) downtime of CMS, I'll extend the deadline for Chapter 2 to the end of the day on Wednesday.

If you still need help with Chapter 2 exercises, please continue to submit questions

Written on 29.11.24 (last change on 08.01.25) by Andrea Lattuada

Dear Students, if you've previously submitted questions on chapter 2 exercises, I should have by now either addressed the question during the tutorial or lecture, or have given you a personal answer as "feedback" to the submission: if that's not the case, please submit again.

I have re-opened the… Read more

Dear Students, if you've previously submitted questions on chapter 2 exercises, I should have by now either addressed the question during the tutorial or lecture, or have given you a personal answer as "feedback" to the submission: if that's not the case, please submit again.

I have re-opened the "Chapter 02: Basics and Specification - Questions" Submission (you can reach it from your "Personal Status" page, like a regular exercise submissions) for you to submit questions on the Chapter 2 exercises. You can upload a txt, rtf, pdf, Word, or zip file (containing multiple of the file types I listed; if you submit something else I can't guarantee I'll be able to open it): you can only submit one file, so if you have multiple questions, add them all to one file / zip file.

I will run the auto-grader every day from now till the deadline, for you to have more opportunities to test your code against the auto-grader.

If you haven't submitted yet, you should do so by the end of the day today, as you only have four more rounds of feedback until the deadline. If you only have a partial solution, submit anyway, to get at least some feedback from the autograder.

 

Submit your questions on Chapter 2 exercises by tomorrow at 12:00

Written on 28.11.24 (last change on 08.01.25) by Andrea Lattuada

Dear Students, I have re-opened the "Chapter 02: Basics and Specification - Questions" Submission (you can reach it from your "Personal Status" page, like a regular exercise submissions) for you to submit questions on the Chapter 2 exercises. You can upload a txt, rtf, pdf, Word, or zip file… Read more

Dear Students, I have re-opened the "Chapter 02: Basics and Specification - Questions" Submission (you can reach it from your "Personal Status" page, like a regular exercise submissions) for you to submit questions on the Chapter 2 exercises. You can upload a txt, rtf, pdf, Word, or zip file (containing multiple of the file types I listed; if you submit something else I can't guarantee I'll be able to open it): you can only submit one file, so if you have multiple questions, add them all to one file / zip file. If you've already submitted,

I have made a copy of all the questions and (hopefully) answered them all during the exercise session yesterday (the recording is available): if you've already submitted and have further questions, feel free to replace your submission with further questions (they're timestamped, so I'll know that you have additional questions, but note that if you then replace the submission again, I'll only see the latest version). If you submit a question, please make sure you have also submitted at least a partial solution to the exercise itself (the "Chapter 02: Basics and Specification" submission), so I can reference your code if needed.

For questions I receive by the end of the day today, I'll give an answer or hint at the start of tomorrow's lecture.

Submit your questions on Chapter 2 exercises by tomorrow at 12:00

Written on 26.11.24 (last change on 08.01.25) by Andrea Lattuada

Dear Students, I have opened another Submission (you can reach it from your "Personal Status" page, like a regular exercise submissions) for you to submit questions on the Chapter 2 exercises (it's called "Chapter 02: Basics and Specification - Questions"). You can upload a txt, rtf, pdf, or Word… Read more

Dear Students, I have opened another Submission (you can reach it from your "Personal Status" page, like a regular exercise submissions) for you to submit questions on the Chapter 2 exercises (it's called "Chapter 02: Basics and Specification - Questions"). You can upload a txt, rtf, pdf, or Word file: you can only submit one file, I believe, so if you have multiple questions, add them all to one file. If you're finding some of the exercises challenging, please let me know through that channel, so I can try and adjust tomorrow's tutorial based on the feedback. Make sure you don't submit questions to the main "Chapter 02: Basics and Specification" submission, as that would score you zero points for Chapter 02, while "Chapter 02: Basics and Specification - Questions" is obviously not graded.

Chapter 1 exercises due on Friday evening. Please reach out directly if there are issues.

Written on 18.11.24 (last change on 08.01.25) 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:

  • we provide feedback on the exercises every other day (we'll provide feedback today, Wednesday, and Friday just after the lecture);
  • Chapter 00 was just a… Read more

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:

  • we provide feedback on the exercises every other day (we'll provide feedback today, Wednesday, and Friday just after the lecture);
  • Chapter 00 was just a test exercise and does not count towards the 7 out of 8 exercises you need to pass to have access to the exam;
  • if you haven't submitted yet, you haven't missed any deadline yet (the first graded exercise is Chapter 01, open till Friday);
  • if you have questions or issues regarding the exercises: please reach out as soon as possible and directly (not via the "feedback" button on CMS, because that anonymizes your comment so I cannot respond -- you're welcome to use the "feedback" button on CMS for any other feedback you want to send anonymously);
  • if you believe that the feedback you received is not correct, please reach out immediately (andrea@mpi-sws.org); do not wait until the deadline, as you won't have the chance to re-submit, in case the feedback is in fact correct;
  • do not change the exercise filenames, do not add comments to the exercises outside the "editable area" markers (/*{*/ /*}*/)

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 (last change on 08.01.25) 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 (last change on 08.01.25) 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.

Here is more info on how to find the rooms.

Let us know which hardware/software configuration you're running by Monday 28th.

Written on 25.10.24 (last change on 08.01.25) 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 08.01.25) 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.

Show all

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

➡️ Course Evaluation

 


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

 

Project 1 will be scored according to the following criteria:

  • Adherence to the English-language specification of the state, steps, and safety property;
  • Understandability of the state machine state and steps (prefer enum/structs; use comments where necessary, but not in excess!);
  • Identification of inductive invariants, and completeness of the safety proof.

You will not get a passing score for the project if you just submit the handout file unchanged (even if it verifies). You will get a higher score if you submit a project that does not verify but has correct, well-written transitions, an accurate and concise safety property, and at least an attempt to identify the inductive invariant and to write the safety proof. A proof that works for only some of the cases (e.g. some of the host steps) is better than an empty proof, or no invariant.

 

Project 2 will be scored according to the following criteria:

  • Adherence to the English-language specification of the state and steps, for both the specification and the distributed protocol (host steps);
  • Understandability of the state machines' state and steps (prefer enum/structs; use comments where necessary, but not in excess!);
  • Identification of interpretation functions, refinement invariant, and completeness of the refinement proof.

 

Project 1 grading progress: 🟩🟩🟩🟩🟩🟩🟩🟩🟩🟩⬜️⬜️⬜️⬜️⬜️⬜️⬜️⬜️⬜️⬜️⬜️⬜️⬜️⬜️⬜️⬜️⬜️
    🟩 passed 🟥 failed ⬜️ ungraded

 

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-15: Specification and state machines
- 2024-11-22: State machines and behaviors
- 2024-11-29: Proving properties and inductive invariants
- 2024-12-06: Leader election demo
- 2024-12-13: Modeling distributed and asynchronous systems

- 2024-12-20: Refinement Introduction + Project 1 assignment

- 2025-01-10: Refinement: Application correspondence, Reduction (Part 1)
- 2025-01-17: Reduction (Part 2) + Project 2 assignment
- 2025-01-24: (Project 2 Office Hours)
- 2025-01-31: Advanced Techniques, Research 
- 2025-02-07: Recap (Optional)

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
  • You are not allowed to use `#[verifier::external_body]` in the code you submit (unless it's already present in the assignment)
  • Do not rename the files

 

Verus logo CC-BY Verus Contributors, Rust logo CC-BY Rust Foundation

Privacy Policy | Legal Notice
If you encounter technical problems, please contact the administrators.