Specification and Verification with Higher Order Logic (3V+3U, 8.0 LP)
|SWS||Type||Course Form||CP (Effort)||Presence-Time / Self-Study|
|-||K||Lecture with exercise classes (V/U)||8.0 CP||156 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|| Master (General)|
|Language||[DE/EN] German or English as required|
|Area of study||[INF-SE] Software-Engineering|
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)None
References to Course [INF-32-52-K-6]
|[INF-32-52-M-6]||Specification and Verification with Higher Order Logic||P: Obligatory||3V+3U, 8.0 LP|