en | de

Experimente mit Verifikation – Einführung in Isabelle/HOL

Masterstudium

VO1  SS 2010  703523

Einführung

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  1: formal verification, Isabelle/HOL basics, functional programming in HOL (functional programming)
Session  2: simplification (term rewriting), function definitions, induction, calculational reasoning
Session  3: natural deduction, propositional logic, predicate logic (logic)
Session  4: (inductively defined) sets, relations, advanced topics

Quellenangabe

In der Lehrveranstaltung wird Material aus der folgenden Quelle verwendet:

Sprache

Die Vorlesung wird auf Englisch abgehalten.