Time Machine Bernd Finkbeiner

Time Machine

This Proseminar is concerned with modeling time in verification. Students will learn how to define temporal properties to specify requirements of real-world systems, like a drone that is supposed to land within five seconds or a green house that should water the plants in regular intervals. We will investigate how to model such real-world systems focusing on their temporal behavior, especially in conjunction with their surroundings. In order to combine properties and models, appropriate decision procedures will be outlined.

This class is designed to teach how to give a scientific presentation. Students will read up on a topic, summarize it, and teach the findings to their fellows in a presentation. After a practice run, students are asked to give feedback, enabling a process of improvement for the final presentation.

Requirements

Talks: We expect you to give two talks on the topics you have been assigned, an ungraded practice talk to provide feedback about the quality of your work so far, and a graded final talk. More information can be found here.

Feedback and Discussion: Attendance to all talks is mandatory. We expect you to provide feedback to your fellow students after the practice talks, and participate in discussions after the final talks.

Summary: At the end of the semester, we expect you to submit a short summary of your paper. More details can be found here.

Language

All background material is only available in English. Even though you are allowed to give your talk and write your summary in German, we advise against it: You are not graded based on your level of mastery in the English language, but your quality of presentation. The universal working language for computer science is English, so it is worthwhile collecting experience writing and speaking English.

Prerequisites

We expect you to understand basic mathematical notation and have the ability to think about abstract concepts. We will provide all further background knowledge.