Lecture on Isabelle and Program Verification
Organization
- Mode: In presence with online recordings of the lecture
- Time: Tuesdays and Thursdays from 10-12am
- 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
Goals
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).
ILIAS
Further details, current news and materials for the lecture will be made available on the ILIAS platform.