Seminar: Formal Specification and Verification

Form: Seminar - 3CP (2 SWS)
Organizer: Prof. Dr. Heiko Mantel
Contact: Dr. Lars Luthmann, Alexandra Weber
Time and Place: Block seminar, tentative dates:
Thursday, 17.6.2021 and Friday, 18.6.2021
Language: English
Registration: in TUCaN (course id 20-00-0914-se)
Max. participants: 15
Preparation meeting (online): Thursday, 15.4.2021, at 15:15
You can find relevant articles here. More details will be provided in the preparation meeting.

Information regarding the Corona pandemic:
This course will happen. In the beginning of the summer semester 2021, 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, 15.4.2021, at 15:15, 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

Please register for the preparation meeting by 14.4.2021.

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.

We have distributed the information how to join the preparation meeting. In case you haven't received the credentials yet, please contact us via as soon as possible.


Materials for the seminar, including the list of articles that we discuss, will be available in Moodle.


As long as requirements to computer designs are formulated in an ambiguous human language and as long as these designs are implemented by humans not insured against possible carelessness and misunderstandings, computer systems will contain errors. For the time being, the only way to guarantee the absence of errors in a computer system is to exploit rigorous formal methods of mathematics for specifying a system's intended behavior and proving that the actual system's implementation meets the desired behavior.

In the seminar, we will consider articles describing how logic and mathematics could be applied for precise specification and subsequent verification of selected computer systems, e.g., processors, compilers, and micro kernels.

Learning Objectives

After successful participation in the course, you become acquainted with an unfamiliar subject by working with scientific papers. You are proficient in different techniques of library research (including accessing special databases). You can compare and contrast research results across multiple publications and perform an overarching evaluation of these results. You recognize the essential aspects of the examined works and are able to concisely present them to an audience with mixed prior experience on the subject, effectively applying a number of presentation techniques in the process. You are able to actively participate in a scientific discussion on the presented topics.


Knowledge of Computer Science equivalent to the first four Semesters in the Computer Science Bachelor program.

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