Lab: Formal Specification and Verification in Isabelle/HOL - SuTe 2021

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
Join the Lab: register via TUCaN, the lab will start with a mandatory online kick-off meeting on
Thursday, 15.4.2021, at 15:15

Course website: https://www.mais.informatik.tu-darmstadt.de/isabelle-ss21.html