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

Basedata

SWS 3V+3U
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
Lecturers
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.

Contents

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

Literature

  • 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)

None

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