Chair of Computer Architecture

University Freiburg

Lecture on Isabelle and Program Verification, Summer 2024


Organization


The course will be based on the slides I have prepared for the tutorial I gave in Vienna, but very expanded.

Goals


There is a verification gap between automatic tools (like SAT or SMT solvers) and what we can prove by hand. This is exactly where interactive proof assistants come in: They allow user to write proofs by hand, while still having (some) automation. No more time out where you start vodoo dancing where variable renaming might make the problem easy to solve!

The interactive theorem prover has a small (trusted) kernel and you do not have to trust severel thousand line of C or C++ code. So you get a lot more trust and a lot more control.

This lectures is about formal proofs using the proof assistant Isabelle/HOL. The first part is a general introduction to the tool, while the second part is focused on program verification (in particular program synthesis from a specification in Isabelle).

Here is what the result of what in Isabelle formalization looks like. Every formalization lecture has several goals:

  1. using the proof assistant and understanding the interface;
  2. managing to write the proofs;
  3. convincing the proof assistant that the proof is correct.

While the proof assistant helps you to write a proof, it write the proof for you. Therefore, if you hate writing proofs, this is not the right lecture for you.

Organisation

The course will be in-person only at least for the first few weeks. After that (and once you are more used to the Isabelle syntax), we will switch to hybrid where we recommand coming and enough people have to activate your camera (or be there in person).

Grading

This lecture is composed of two parts:

The deadline for the project will be two weeks after the end of the lecture (so before the beginning of the exam period as required by the university rules – but I am open to discussion if you want to take two weeks off).

Experience from past courses tells that success in the exercises is necessary to succeed in the exam (and so far I have never anyone who did the exercises fail in the project).

There will be no written “exam”: the project is the exam which decides the grade.

ILIAS


Further details, current news and materials for the lecture will be made available on the ILIAS platform.