| Lab | Branch |
|---|---|
| 1 | lab1 |
| 2 | lab2 |
| 3 | lab3 |
| 4 | lab4 |
| 5 | lab5 |
This repository is the homepage of the course Formal Verification and hosts the material necesary for the labs.
- Professor: Viktor Kunčak
- Teaching Assistant: Simon Guilloud
- Student Assistant: Dario Halilovic
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 in November (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 2023 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.
To see the material, please visit https://mediaspace.epfl.ch , log in with your EPFL credentials and select this channel. Slides and listings are attached underneath the videos.
| Week | Day | Date | Time | Room | Topic | Videos & Slides |
|---|---|---|---|---|---|---|
| 1 | Thu | 12.09.2024 | 15:15 | GRA330 | Lecture 1 | Intro to FV, Intro to Stainless, Auxiliary Assertions, Unfolding, Disasters, Successes, and Inductive Invariants |
| 17:15 | GRA330 | Lecture 2 | Dispenser Example, Finite Systems Expressed with Formulas | |||
| Reading: | HandMC-Ch.10 | |||||
| Follow: | Stainless Tutorial Videos and materials | |||||
| Fri | 13.09.2024 | 13:15 | INR219 | Lecture 3 | What is a Formal Proof? and Propositional Resolution | |
| 2 | Thu | 19.09.2024 | 15:15 | GRA330 | Lecture 4 PDF | continue Propositional Resolution |
| 17:15 | GRA330 | Lab 1 | ||||
| Fri | 20.09.2024 | 13:15 | INR219 | Exercises 1 | Propositional Logic | |
| Reading: | CalComp-Ch.1 ∨ HandAR-Ch.2 | |||||
| 3 | Thu | 26.09.2024 | 15:15 | GRA330 | Lecture 5 PDF | SAT solving from Propositional Resolution. Start Automating First-Order Logic Proofs Using Resolution |
| 17:15 | GRA330 | Lab 2 | A communication protocol in Stainless | |||
| Reading: | HandAR-Ch.3 | |||||
| Fri | 27.09.2024 | 13:15 | INR219 | Exercises 2 | Traces, SAT, models | |
| 4 | Thu | 03.10.2024 | 15:15 | GRA330 | Lecture 6 PDF | Continue Automating First-Order Logic using Resolution. Term Models for First-Order Logic |
| 17:15 | GRA330 | Lab 3 | FOL Resolution | |||
| Provers Proved New Math Results (also in NYT), SPASS Prover on The Web | ||||||
| Reading: | HandAR-Ch.3 | |||||
| Fri | 04.10.2024 | 13:15 | INR219 | Exercises 3 | ||
| 5 | Thu | 10.10.2024 | 15:15 | GRA330 | Lecture 7: vcgen.pdf Hoare.pdf | Converting Imperative Programs to Formulas, Hoare Logic, Strongest Postcondition, Weakest Precondition |
| Fri | 11.10.2024 | 13:15 | INR219 | Exercises 4 | Transition Systems, Hoare Logic, Relations | |
| 6 | Thu | 17.10.2024 | 15:05 | GRA330 | Lecture | Guest Lecture of Gilles Barthe |
| 6 | Thu | 17.10.2024 | 16:15 | GRA330 | Lab 4 | Using Lisa Proof Framework |
| 17:15 | GRA330 | Lecture 8 PDF | Quantifier Elimination | |||
| Fri | 18.10.2024 | 13:15 | INR219 | Exercises 5 | Quantifier elimination exercises | |
| - | Thu | 24.10.2024 | 15:15 | Holidays | ||
| 17:15 | Holidays | |||||
| Fri | 25.10.2024 | 13:15 | Holidays | |||
| 7 | Thu | 31.10.2024 | 15:15 | GRA330 | Lecture 9 PDF | Abstract Interpration. Lattices. Tarski's fixpoint theorem |
| 17:15 | GRA330 | Labs | ||||
| Deadline to pick your project topic and Background Paper | ||||||
| Fri | 01.11.2024 | 13:15 | INR219 | Exercises 6 | ||
| 8 | Thu | 07.11.2024 | 15:15 | GRA330 | Lecture 10 PDF | Fixed Points. Predicates |
| 17:15 | GRA330 | Labs | ||||
| Deadline to write your Background Paper Review | ||||||
| Fri | 08.11.2024 | 13:15 | INR219 | Exercises 7 | ||
| 9 | Thu | 14.11.2024 | 15:15 | GRA330 | ||
| 17:15 | GRA330 | |||||
| Fri | 15.11.2024 | 13:15 | INR219 | |||
| 10 | Thu | 21.11.2024 | 15:15 | GRA330 | ||
| 17:15 | GRA330 | |||||
| Fri | 22.11.2024 | 13:15 | INR219 | |||
| 11 | Thu | 28.11.2024 | 15:15 | GRA330, AAC114 | Midterm, until 18:00 | |
| Fri | 29.11.2024 | 13:15 | INR219 | |||
| 12 | Thu | 05.12.2024 | 15:15 | GRA330 | ||
| 17:15 | GRA330 | |||||
| Fri | 06.12.2024 | 13:15 | INR219 | |||
| 13 | Thu | 12.12.2024 | 15:15 | GRA330 | ||
| 17:15 | GRA330 | |||||
| Fri | 13.12.2024 | 13:15 | INR219 | |||
| 14 | Thu | 19.12.2024 | 15:15 | GRA330 | ||
| 17:15 | GRA330 | |||||
| Fri | 20.12.2024 | 13:15 | INR219 |
Midterm exam: Thursday, 28 November, 15:00-18:00