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
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.
- learn to use state-of-the-art in tools for formal modeling and interactive theorem proving
- structured content – 8 assignments
- weekly supervision