Scientific Colloquium on the occasion of the 60th Birthday of Prof. Tobias Nipkow, Ph. D.

Friday, 20th July 2018 Department of Informatics, Boltzmannstr. 3 , 85748 Garching

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.

View Pictures


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 You may revoke this permission by sending an email to


Contact Person I 21 Chair for Logic and Verification Prof. Nipkow:

Helma, Phone: +49-89-289-17300


Contact Person Public Relations:

Doris, Phone: +49-89-289-17928