The proof, the whole proof, and nothing but the proof. The proof, the HOL proof, and nothing but the proof.
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 17301
- Office:
- MI 00.09.055
(Boltzmannstr. 3, Garching) - Administrative Assistants:
- Eleni Nikolaou-Weiß <{weissel} AT [in.tum.de]>
MI 00.09.053
Phone: +49 89 289 17300
Fax: +49 89 289 17301
You can also write email directly to any other member of the team.
The chair is actively involved in co-organizing the Marktoberdorf Summer School.
News
- We changed rooms, our chair is now at floor 00.09.
- Congratulations! Jasmin C. Blanchette has won the “Schwärtzel-Dissertationspreis für Grundlagen der Informatik” for his Ph.D. thesis “Automatic Proofs and Refutations for Higher-Order Logic”.
- Isabelle won the Higher-Order divison of the 2012 annual competition of automated theorem provers (CASC-J6). Congretulations to Jasmin Blanchette who developed the Isabelle-based prover. For details of the results see here.
- 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!