Formal Specification and Verification in Isabelle/HOL

Organizer:	Prof. Dr. Heiko Mantel
Registration:	via TUCaN (20-00-0778-pr), Miriam Rifai-Schön (S2|02 E318), or Jinwei Hu, Ph.D. (S2|02 E322)
Preparation Meeting:	16 Oct 2014 (Thu), 16:00 at S202 E302
Regular Meeting:	Mondays, 14:25-16:05 at S2|02 E302, starting from 20 Oct 2014

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, which is one of the internationally leading tools. Formal models of increasing conceptual complexity will be defined in Isabelle's higher-order logic and Isabelle's semi-automatic verification engine will used to verify properties.

The topics covered by this course include:

• designing formal models of systems
• specifying properties of systems
• identifying advantages and disadvantages of a chosen model, and
• verifying the models against the specified properties.

 

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

Internal Area

Materials for participants are available in the internal area.

Updates inside the internal area:

Assignments

• 2014-10-20: Assignment 1
• 2014-10-27: Assignment 2
• 2014-11-03: Assignment 3
• 2014-11-03: Assignment 3
• 2014-11-10: Assignment 3 v1.1
• 2014-11-10: Assignment 4
• 2014-11-17: Assignment 5
• 2014-12-03: Assignment 6
• 2014-12-14: Assignment 7

Sample solution

• 2014-11-10: Assignment 3
• 2014-11-17: Assignment 4 (part 1)
• 2014-11-17: Assignment 4 (Automata)
• 2014-11-26: Assignment 2 Solutions
• 2014-11-26: Assignment 4
• 2014-11-26: Assignment 5 (5.1)
• 2014-12-08: Assignment 5 (5.2)
• 2014-12-17: A While language with more intuitive syntax

Last modified on 22 November 2016.