How can I prove equations automatically? How can I verify correctness of a Java compiler? How can I be sure that Kepler was right? How can I prove automatically that some weird and wonderful search tree variant has the desired functionality?
These are some of the research questions that have kept Tobias Nipkow busy at Manchester University, MIT, Cambridge University and as a professor at TUM since 1992. This colloquium presents recent results on automated and interactive theorem proving, the central research areas of Tobias Nipkow.
2.00 pm Drinks (in front of lecture hall 2)
2.45 pm Program Start in lecture hall 2
Opening by Hans-Joachim Bungartz, Dean of the Department of Informatics
3.00 pm Welcome by Hans Pongratz, CIO TUM
3.15 pm Gerwin Klein: "seL4: Formal Verfication at Scale"
3.50 pm Break with Drinks & Coffee
4.20 pm Andreas Lochbihler: "Mechanising a type-safe model of multithreaded Java with a verified
4.55 pm Jasmin Blanchette: "A Verified SAT Solver Using Imperative HOL"
5.30 pm Drinks
6.00 pm Dinner
Registration is requested before 12 July 2018 via
Please email us
- your postal address
- the number of accompanying persons
Please note that we will take photos during the event. By visiting this event you agree with the photos being published on our department’s website in.tum.de. You may revoke this permission by sending an email to Doris.Herrmann@tum.de
Contact Person I 21 Chair for Logic and Verification Prof. Nipkow:
Helma Piller, firstname.lastname@example.org, Phone: +49-89-289-17300
Contact Person Public Relations:
Doris Herrmann, Doris.Herrmann@tum.de, Phone: +49-89-289-17928