en | de

Experimente mit Verifikation – Einführung in Isabelle/HOL

Masterstudium

VO1  SS 2011  703523

Inhalt

Die Lehrveranstaltung gibt eine Einführung in den Beweisassistenten Isabelle/HOL.

Zeitplan

Die Vorlesung wird geblockt abgehalten. Statt einer wöchentlichen 1-stündigen Vorlesung, finden 4 Sessions zu je 3 Stunden statt. Kurse, die einige der in der VO besprochenen Inhalte vertiefen, sind in Klammern aufgeführt.

Session Datum Themen Folien Quelltext
1 11.03. formal verification, Isabelle/HOL basics, functional programming in HOL (functional programming) pdf (4x1) Archiv
2 25.03 simplification (term rewriting), function definitions, induction, calculational reasoning pdf (4x1) Archiv
3 01.04. natural deduction, propositional logic, predicate logic (logic) pdf (4x1) Archiv
4 15.04. (inductively defined) sets, relations, advanced topics pdf (4x1) Archiv

Quellenangabe

In der Lehrveranstaltung wird Material aus der folgenden Quelle verwendet: