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.

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.

Week Lecture Exercise Remarks Main objective
17.04 Introduction, functional programming in Isabelle (goat/wolf problem)   Writing programs
24.04 Writing lemmas, nitpick, syntax No lecture (AIG+polynomial)   Writing properties
01.05 No lecture   Tag der arbeit Writing structured proofs
08.05 Proofs per hand in Isar No exercise    
15.05 Tactics (finally proving with Isabelle) (AIG+polynomial)   Proving in Isabelle
22.05     Pfingstpause  
29.05 Isar No exercise   Writing structured proofs
05.06 Inductive processes + Sledgehammer   Decision about project Program verification
12.06 Code generation + Locale for data structure refinement LRAT verification    
19.06 Refinement Framework LRAT verification    
26.06 No lecture LRAT verification    
03.07 Refinement Framework + slack      
10.07 Sepref      
17.07 Q&A project + feedback discussion official Project start    

ILIAS


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