Organizer: | Prof. Dr. Heiko Mantel | |
Contact: | teachingmais.informatik.tu-darmstadt.de |
|
Assistant: | Tim Weißmantel |
|
Form: | Lab Course (P4) - 6CP |
|
Language: | English | |
Weekly meeting: | Friday 13:30 - 15:10 in S2|15 404K |
|
Registration: | in TUCaN (course id 20-00-0778-pr) | |
Max. participants: | 15 |
|
Preparation meeting: | Tuesday, April 19 at 14:25 (online or offline) Depending on the number of participants the meeting will either happen online or offline. Please register for this course via TUCaN or write an e-mail to teachingmais.informatik.tu-darmstadt.de to receive information about the physical location or Zoom credentials. |
|
Workload: | Separate assignment sheets, no single monolithic project |
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:
Knowledge of Computer Science and Mathematics, equivalent to the first four semesters in the Computer Science Bachelor program, in particular ability to work with formal languages and calculi, and knowledge of propositional and predicate logic.
Last modified on 1 April 2022.