Lab: Formal Specification and Verification in Isabelle/HOL

Organizer: Prof. Dr. Heiko Mantel
Assistants: Tobias Hamann
Alexandra Weber

Form: Lab Course (P4) - 6CP
Language: English
Weekly meeting: Wednesday 13:30-15:10  (S217/103)
Registration: in TUCaN (course id 20-00-0778-pr)
Preparation meeting (online): Thursday, 23.4.2020, at 16:00
please register for the course via TUCaN or write a short e-mail to kickoff-2020@mais.informatik.tu-darmstadt.de to receive information via e-mail how to join the preparation meeting
please register by Thursday, 23.4.2020, 12:00
Workload: Separate assignment sheets, no single monolithic project

 

Information regarding the Corona pandemic:
This course will happen. In the beginning of the summer semester 2020, this course will be taught online. We closely monitor the situation and adapt the format of this course accordingly throughout the semester. The official start of this course is the online preparation meeting on Thursday, 23.4.2020, at 16:00, in which you will receive more information about this course's format. We will provide more information how to join the preparation meeting via e-mail before. To receive this e-mail, please register for this course via TUCaN or write an e-mail to kickoff-2020@mais.informatik.tu-darmstadt.de.

Please register for the preparation meeting by Thursday, 23.4.2020, 12:00

On-line participation in the preparation meeting is required for all labs and seminars. The registration in the courses gets only effective after steps explained in the preparation meeting.

 

Content

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.


Prerequisites

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.

Literature


Last modified on 27 August 2020.

A A A | Print | Imprint | Sitemap | Contact
zum Seitenanfang