Seminar: Formal Specification and Verification

Organizer:	Prof. Dr. Heiko Mantel
Form:	Seminar (S2) - 3 CP
Language:	English
Dates:	Block seminar on December 3-4, 2015, 9:00-20:00, in S2|02 E302 (please reserve both days, the exact schedule will be determined depending on the actual number of participants)
Registration:	in TUCaN (course id 20-00-0914-se)
Preparation meeting:	October 14, 2015, 16:15-17:55, in S2|02 E302

 

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.

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 18 December 2015.