Chair of Computer Architecture

Lecture on Isabelle and Program Verification, Summer 2024

Organization

• Mode: In presence
• Time: Wednesday (10:15 to 11:45) and Thursday (12:15 to 13:45)
• Credits: 6 ECTS (2+2 hours)
• Dependencies: knowing how to do induction on paper
• Responsible: Prof. Dr. Armin Biere (on paper, never write him an email about the lecture!)
• Support: Dr. Mathias Fleury
• Exercises: mandatory exercises

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 weekly exercise that count for the studienleistung (convincing a computer that your proof is correct requires getting used to it)

• a project at the end. There are two options to be discussed during the class (around week 6 or 7 of the semester): either every one tries to formalize something (whatever) or we all work together on a bigger project (like a simple DPLL solver or something like that).

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.

Program

The program below is a plan. It is not final and especially the part on “Writing structured proofs” might have to be extended, because nothing is possible without it in the next part of the course. The exercise are given as idea and are not final yet.

We will probably not do any Refinement Framework this year.

ILIAS

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