Chair of Computer Architecture

University of Freiburg

Lecture on Isabelle and Program Verification



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).


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