Time Machine Bernd Finkbeiner

Registration for this course is open until Thursday, 19.10.2017 23:59.



Dear students,

we decided to avoid having a meeting in the last week of October due to two consecutive public holidays. 
Please check out the Important Dates page for the new schedule.


Extended Registration

Dear students, 

we extended the registration period to October 19 and moved the Kick-Off and Background Meeting by one week each. They will take place at 10am on Monday, October 23 and October 30, respectively. 



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.


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.


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.


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

If you encounter technical problems, please contact the administrators