Module Handbook

  • Dynamischer Default-Fachbereich geändert auf INF

Course INF-32-52-K-6

Specification and Verification with Higher Order Logic (3V+3U, 8.0 LP)

Course Type

SWS Type Course Form CP (Effort) Presence-Time / Self-Study
- K Lecture with exercise classes (V/U) 8.0 CP 156 h
3 V Lecture 42 h
3 U Exercise class (in small groups) 42 h
(3V+3U) 8.0 CP 84 h 156 h


CP, Effort 8.0 CP = 240 h
Position of the semester 1 Sem. irreg.
Level [6] Master (General)
Language [DE/EN] German or English as required
Area of study [INF-SE] Software-Engineering
Livecycle-State [NORM] Active

Possible Study achievement

  • Verification of study performance: proof of successful participation in the exercise classes (ungraded)
  • Details of the examination (type, duration, criteria) will be announced at the beginning of the course.


The lecture is about:
  • Constructs for functional programming and specification
  • Higher-order logic
  • Terms, theorems, rules, tactics as constructs of software technology
  • Writing specifications
  • Tactical theorem proving


  • M. J. C. Gordon and T. F. Melham, Introduction to HOL: A Theorem Proving Environment for Higher Order Logic, Cambridge University Press, 1993.
  • T. Nipkow, L. C. Paulson and M. Wenzel, Isabelle/HOL - A Proof Assistant for Higher-Order Logic, Springer LNCS 2283, 2002.

Requirements for attendance (informal)

Compulsory modules of the Bachelor of Computer Science

Basics of the specialization "Algorithmics and Deduction"

Requirements for attendance (formal)


References to Course [INF-32-52-K-6]

Module Name Context
[INF-32-52-M-6] Specification and Verification with Higher Order Logic P: Obligatory 3V+3U, 8.0 LP