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 |
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:
Knowledge of Computer Science and Mathematics, equivalent to the first four semesters in the Computer Science Bachelor program, in particular
Last modified on 22 November 2016.