MAIS

Seminar: Formal Specification

Form:	Seminar - 3CP (2 SWS)
Organizer:	Prof. Dr. Heiko Mantel
Contact:	Tobias Hamann
Time and Place:	TBD
Language:	English
Registration:	in TUCaN (course id 20-00-0914-se)
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

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

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 contains errors. For the time being, the only way to guarantee absence of errors in a computer system is to exploit rigorous formal methods of mathematics for specifying 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 microkernels. In this semester, the focus of the considered articles is on policy languages for expressing system requirements.

Participants of the seminar can use an opportunity to apply the studied techniques in the lab course "Formal Specification and Verification in Isabelle/HOL" that will take place in the same semester. However, the seminar and the lab course can also be taken individually.

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.

Prerequisites

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

Last modified on 27 August 2020.