Mission
Our research is about applications of logic to programming. The goal is to prove program properties by logical deductions and to build tools that support and automate these deductions. To this end we are developing the theorem prover Isabelle in close connection with Makarius Wenzel (Université Paris-Sud) and Larry Paulson (University of Cambridge) who is also Distinguished Affiliated Professor in our department.
Isabelle is a so called interactive theorem prover. It supports the proof of arbitrary mathematical theorems in a dialogue between user and machine. The user describes the overall structure of the proof in a programming language like notation, the system checks the correctness of each step and tries to fill in missing details.
Contact
- Address:
- Prof. Tobias Nipkow <{nipkow} AT [in.tum.de]>
Institut für Informatik, Lehrstuhl XXI
Technische Universität München
Boltzmannstr. 3
D-85748 Garching
Germany - Phone:
- +49 89 289 17302
- Fax:
- +49 89 289 17307
- Office:
- MI 01.11.058
(Boltzmannstr. 3, Garching) - Secretary:
- Eleni Nikolaou-Weiß <{weissel} AT [in.tum.de]>
MI 01.11.042
Phone: +49 89 289 17311
Fax: +49 89 289 17307
You can also write email directly to any other member of the team.
News
- The Theorem Proving Group is now the Chair for Logic and Verification (Lehrstuhl für Logik und Verifikation).
- The list of 10 emerging technologies that MIT's Technology Review think will have the greatest impact for 2011 contains NICTA's operating system kernel verification led by Gerwin Klein, which uses Isabelle.
- Congratulations! Alex Krauss has won the »Schwärtzel-Dissertationspreis für Grundlagen der Informatik« for his Ph.D. thesis »Automating Recursive Definitions and Termination Proofs in Higher-Order Logic«.
- Congratulations! Lukas Bulwahn has won the »Siemens-Preis« for his Diploma thesis »Code Generation from Inductive Predicates in Isabelle/HOL«.
- Robot software verified with Isabelle.
- Our former team member Gerwin Klein has lead the first ever verification of a general-purpose operating system kernel – using Isabelle! Read the award-winning SOSP paper.
- Larry Paulson became Distinguished Affiliated Professor for Logic in Informatics at TUM!
- Our former team member Gerwin Klein was awarded the GI dissertation prize for his thesis about verifying the Java bytecode verifier in Isabelle/HOL!
The chair is actively involved in co-organizing the Marktoberdorf Summer School.