This repository is the homepage of the course Formal Verification (autumn 2023) and hosts the material necesary for the labs.
- Professor: Viktor Kunčak
- Teaching Assistant: Simon Guilloud
- Student Assistants: Andrea Gilot, Valentin Aebi, Noé De Santo
The grade is based on the written mid-term, as well as code, documentation, and explanation of projects during the semester. Specific percentages will be communicated in the first class and posted here.
The types of graded materials will include:
- 40% Late mid-term written exam: 23 November 15:15-18:00 (see this folder with past exams)
- 20% total: four-five labs, to be done in groups, each group working independently on same projects
- 40% final project to be done in groups, you will choose a topic with our agreement
- 10% Written presentation of a background paper
- 10% Results accomplished (how hard it was, how far you got)
- 10% Presentation of results
- 10% Final report
In this course we introduce formal verification as a principled approach for developing systems that do what they should do.
The course has two aspects:
- learning the practice of formal verification - how to use tools to construct verified software
- understanding the principles behind formal verification and the ways in which verification tools work
The course will follow a similar structure to the 2022 edition. Project can be a case study in developing a verified piece of software, an implementation of verification tool functionality, or a theoretical result about verification, constraint solving or theorem proving. Students present their projects with a written report as well as by a live presentation of project results, answering our questions.
Note that slides can be found underneath each lecture video on switch tube linkes below.
- [CalComp] The Calculus of Computation - Decision Procedures with Applications to Verification, 2007, from Springer, from EPFL library, by Aaron Bradley and Zohar Manna.
- [HandMC] Handbook of Model Checking, 2018, from from Springer, from EPFL Library, edited by Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, Roderick Bloem.
- [HandAR] Handbook of Practical Logic and Automated Reasoning, 2009, from Cambridge University Press and from EPFL Library, by John Harrison
In the reading list below, HandAR-Ch.2 means Chapter 2 in the Handbook of Practical Logic and Automated Reasoning Above, whereas HandMC-Ch.9 means Chapter 9 of the Handbook of Model Checking, etc.
| Week | Day | Date | Time | Room | Topic | Videos & Slides |
|---|---|---|---|---|---|---|
| 1 | Thu | 21.09.2023 | 15:15 | GRA330 | Lecture 1 | Intro to FV, Intro to Stainless, Auxiliary Assertions, Unfolding, Disasters, Successes, and Inductive Invariants |
| Follow: | Stainless ASPLOS'22 Tutorial | |||||
| 17:15 | GRA330 | Lecture 2 | Dispenser Example, Finite Systems Expressed with Formulas | |||
| Reading: | HandMC-Ch.10 | |||||
| Fri | 22.09.2023 | 13:15 | INR219 | Lecture 3 | What is a Formal Proof? and Propositional Resolution | |
| Reading: | CalComp-Ch.1 ∨ HandAR-Ch.2 | |||||
| 2 | Thu | 28.09.2023 | 15:15 | GRA330 | Exercise 1 | Propositional logic |
| 17:15 | GRA330 | Lab 1 | Sublists in Stainless | |||
| Fri | 29.09.2023 | 13:15 | INR219 | Lecture 4 | Propositional Resolution up to and including equisatisfiability | |
| 3 | Thu | 5.10.2023 | 15:15 | GRA330 | Lecture 5 | Propositional Resolution: Tseytin's transformation and SAT solving. Automating First-Order Logic using Resolution |
| 17:15 | GRA330 | Lab 2 | A communication protocol in Stainless | |||
| Fri | 6.10.2023 | 13:15 | INR219 | Exercise 2 | Traces, SAT, models | |
| 4 | Thu | 12.10.2023 | 15:15 | GRA330 | Lecture 6 | Continue Automating First-Order Logic using Resolution. Term Models for First-Order Logic |
| 17:15 | GRA330 | Lab 3 | Resolution proof checker (with Stainless) | |||
| Fri | 13.10.2023 | 13:15 | INR219 | Exercise 3 | Propositional logic. Transition systems. Models | |
| 5 | Thu | 19.10.2023 | 15:15 | GRA330 | Lecture 7 | Converting Imperative Programs to Formulas, Hoare Logic, Strongest Postcondition, Weakest Precondition |
| 17:15 | GRA330 | Lab 3 | Continue resolution proof checker | |||
| Fri | 20.10.2023 | 13:15 | INR219 | Lecture 8 | Presburger Arithmetic 1, Presburger Airhtmetic 2 | |
| 6 | Thu | 26.10.2023 | 15:15 | GRA330 | Exercises 4 | |
| 17:15 | GRA330 | Lab 4 | First Lisa Lab | |||
| Fri | 27.10.2023 | 13:15 | INR219 | Lecture 9 | Abstract Interpretation Idea, Lattices | |
| 7 | Thu | 2.11.2023 | 15:15 | GRA330 | Exercises 5 | |
| 17:15 | GRA330 | Lab 5 | ||||
| Fri | 3.11.2023 | 13:15 | INR219 | Lecture 10 | Fixed Point Theorem, Omega Continuity (only until AI recipe) | |
| Sun | 5.11.2023 | Deadline to submit the topic of your project and the background paper you will review | ||||
| 8 | Thu | 9.11.2023 | 15:15 | GRA330 | Exercises 6 | |
| 17:15 | GRA330 | Finish Lab 5, Background paper review, Work on project | ||||
| Fri | 10.11.2023 | 13:15 | INR219 | Lecture 11 | Omega Continuity (from AI recipe onwards), Predicate Abstraction. Complete slides, Annotated | |
| 9 | Thu | 16.11.2023 | 15:15 | GRA330 | Lecture 12 | Monotonicity and Semantics of Local Variables, Relational Semantics of Loops, Loop Semantics Example |
| 17:15 | GRA330 | Work on project | Deadline to finish and upload the background paper review. | |||
| Fri | 17.11.2023 | 13:15 | INR219 | Exercises 7 | ||
| 10 | Thu | 23.11.2023 | 15:15 | GRA330 | WRITTEN EXAM | Exam 2023 Sheet |
| 17:15 | GRA330 | WRITTEN EXAM | ||||
| 11 | Thu | 30.11.2023 | 15:15 | GRA330 | Labs | Project discussions with course staff |
| 17:15 | GRA330 | Exercises | Exam Solutions | |||
| Fri | 01.12.2023 | 13:15 | INR219 | Lecture | Approximating Loops. Recursion 1, Recursion 2, Termination | |
| 12 | Thu | 07.12.2023 | 15:15 | GRA330 | Labs | Project discussions with course staff |
| 17:15 | GRA330 | Labs | Project discussions with course staff | |||
| Fri | 08.12.2023 | 13:15 | INR219 | Lecture | SMT Solvers, Tableau-Based Theorem Proving (by Simon) | |
| 13 | Thu | 14.12.2023 | 15:15 | GRA330 | Lecture | Guest lecture by Prof. Thomas Bourgeat |
| 17:15 | GRA330 | Labs | ||||
| Fri | 15.12.2023 | 13:15 | INR219 | Project Presentations | ILIESCU Valentina-Florentina, WINDLER Leon, LAZAR David Leonardo | |
| 14 | Thu | 21.12.2023 | 15:15 | GRA330 | Project Presentations | GILLIARD Patrick, SCHNEUWLY Victor, PIVETEAU Alexandre |
| 15:45 | GRA330 | Project Presentations | HALILOVIC Dario, HERNANDEZ CANO Alejandro | |||
| 16:15 | GRA330 | Project Presentations | RAZGALLAH Hédi, ROVELLI Gianmaria, KLEYMANN David | |||
| 16:45 | GRA330 | Project Presentations | KAPPELER Kelvin, JOLIDON Bastien, KALLAND Magnus | |||
| 17:15 | GRA330 | Project Presentations | VIDIGUIERA Manuel, CONTOVOUNESIOS Basil, POIROUX Auguste | |||
| Fri | 22.12.2023 | 13:15 | INR219 | Project Presentations | REMMAL Hamza, FLESSELLE Eugene | |
| 13:45 | INR219 | Project Presentations | ZHAO Yaoyu, FALTINGS Victor, BARMETTLER Lars | |||
| 14:15 | INR219 | Project Presentations | WOJNAROWSKI Marcin, BARTRINA Guillem, SAINAS Franco | |||
| 14:45 | INR219 | Project Presentations | DE CASTELNAU Julien, BELENTEPE Cemalettin Cem |