Lab: Formal Specification and Verification in Isabelle/HOL

Organizer:	Prof. Dr. Heiko Mantel
Form:	Lab Course (P4) - 6CP
Language:	English
Weekly meeting:	Mondays, 14:25-16:05, in S1|05 23, starting from October 19, 2015 Exceptions: on November 23, 2015 and February 8, 2016 - in S2|04 213
Registration:	in TUCaN (course id 20-00-0778-pr)
Max. participants:	20
Preparation meeting:	October 14, 2015, 16:15-17:55, in S2|02 E302
Workload:	8 assignments, no single monolithic project

Assignments and other relevant material are posted in Moodle.

Content

Formal methods allow one to model critical requirements precisely and to certify with mathematical rigor that such requirements are met by a system. For applying formal methods to real world problems, tool support is essential. This lab course introduces how to use the Isabelle/HOL tool that is one of the internationally leading tools. Formal models of increasing conceptual complexity will be defined in Isabelle's higher-order logic, so that Isabelle's semi-automatic verification engine may subsequently be used to verify the desired properties. The topics covered by this course include:

• techniques for modeling systems in higher-order logic,
• techniques for specifying desired systems properties,
• design of formal models for systems,
• evaluation of advantages and disadvantages of a chosen model.

Participants of the lab can use an opportunity to learn more about methods of formal specification and verification in the seminar "Formal Specification and Verification" that will take place in the same semester. However, the seminar and the lab course can also be taken individually.

Prerequisites

Knowledge of Computer Science and Mathematics, equivalent to the first four semesters in the Computer Science Bachelor program, in particular ability to work with formal languages and calculi, and knowledge of propositional and predicate logic.

Literature

• Isabelle/HOL: A Proof Assistant for Higher-Order Logic; Springer LNCS 2283 (an updated version is available as tutorial here)
• documentation material on Isabelle and Higher-Order Logic (HOL)

Last modified on 22 November 2016.