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.
Why participate in this lab?
Join the Lab: register via TUCaN, the lab will start with a mandatory kick-off meeting on
- learn to use state-of-the-art in tools for formal modeling and interactive theorem proving
- structured content – 8 assignments
- weekly supervision
Tuesday, 19.4.2022, at 14:25
Course website: https://www.mais.informatik.tu-darmstadt.de/isabelle-sute22.html
- Dozent*in: Heiko Mantel
- Dozent*in: Alexandra Weber
- Dozent*in: Tim Weißmantel