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.
Why participate in this lab?
  • learn to use state-of-the-art in tools for formal modeling and interactive theorem proving
  • structured content – 8 assignments
  • weekly supervision
How to join the lab: register via TUCaN, the lab will start with a kick-off meeting (date TBA)