Module Handbook

  • Dynamischer Default-Fachbereich geändert auf INF

Module INF-32-52-M-6

Specification and Verification with Higher Order Logic (M, 8.0 LP)

Module Identification

Module Number Module Name CP (Effort)
INF-32-52-M-6 Specification and Verification with Higher Order Logic 8.0 CP (240 h)

Basedata

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
Module Manager
Lecturers
Area of study [INF-SE] Software-Engineering
Reference course of study [INF-88.79-SG] M.Sc. Computer Science
Livecycle-State [NORM] Active

Courses

Type/SWS Course Number Title Choice in
Module-Part
Presence-Time /
Self-Study
SL SL is
required for exa.
PL CP Sem.
3V+3U INF-32-52-K-6
Specification and Verification with Higher Order Logic
P 84 h 156 h
U-Schein
ja PL1 8.0 irreg.
  • About [INF-32-52-K-6]: Title: "Specification and Verification with Higher Order Logic"; Presence-Time: 84 h; Self-Study: 156 h
  • About [INF-32-52-K-6]: The study achievement "[U-Schein] proof of successful participation in the exercise classes (ungraded)" must be obtained.
    • It is a prerequisite for the examination for PL1.

Examination achievement PL1

  • Form of examination: oral examination (20-60 Min.)
  • Examination Frequency: irregular (by arrangement)
  • Examination number: 63252 ("Specification and Verification with Higher Order Logic")

Evaluation of grades

The grade of the module examination is also the module grade.


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

Competencies / intended learning achievements

On successful completion of the module, students will be able to
  • explain the basics of interactive theorem provers such as HOL or Isabelle/HOL
  • to derive the syntax and semantics of higher order logic,
  • explain the structure of interactive theorem provers
  • to demonstrate the practical use of interactive theorem provers using examples,
  • to relate different approaches to software verification to each other,
  • to classify algorithmic problems in terms of their complexity and to derive corresponding solution methods,
  • to be able to model complex problems in an appropriate formal way,
  • Languages for design at higher levels of abstraction to be applied exemplarily to problems.

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 of the module (informal)

None

Requirements for attendance of the module (formal)

None

References to Module / Module Number [INF-32-52-M-6]

Course of Study Section Choice/Obligation
[INF-88.79-SG] M.Sc. Computer Science [Specialisation] Specialization 1 [WP] Compulsory Elective