Seminar on Machine-Checked Correctness Proofs for Systems

We will read and discuss papers at the intersection of formal verification and systems.

The learning objective of this seminar is to be able to read, understand, and think critically about papers that apply formal methods to systems research, and to understand what it actually means when a paper claims "we have proved X".

Discussion of each technique presented in a paper will revolve around questions like the following: What parts of the system and toolchain are implicitly assumed to be correct, i.e. what is in the trusted code base? How generalizable is the technique, and how hard would it be to apply it to other examples or other domains? How automated is the technique, how much user interaction does it require? How expressive is the language of assertions that the technique uses? Are there desirable properties that cannot be expressed in its assertion language? Does restricting the expressivity improve automation or verification performance? What is the workflow and the kind of support users get if the tool cannot prove a property? If you were to start research in the same area as the paper being discussed, how would you do it? What would you do differently from the paper you just read?

Students will present papers in teams of two, and each student will present twice. Each presentation will be followed by a discussion moderated by the presenters.

Course Data

Time: Monday, 16:15-18:00

Place: CAB G 56

Lecturer: external page Samuel Gruetter

Course Catalogue Entry: 252-3126-00L Seminar on Machine-Checked Correctness Proofs for Systems

Recommended background: 252-0058-00L Formal Methods and Functional Programming

Active participation (paper presentation and participating in discussion) is required.