en | de

Experiments in Verification – Introduction to Isabelle/HOL

master program

VO1  SS 2010  703523

Introduction

The lecture is blocked. Instead of a weekly 1-hour lecture, there will be 4 sessions of 3 hours each. Related courses to some of the discussed topics are given in parentheses.

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

References

The course incorporates material from the following source:

Language

The lecture is taught in English.