The proof, the whole 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 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.
We're a flexible, client-driven organization!
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:
- Helma Piller
{piller} AT [in.tum.de]
MI 00.09.053
Phone: +49 89 289 17300
Fax: +49 89 289 17301
You can also write an email directly to any other member of the team.
News
-
Congratulations!
ACM Software System Award 2022 for the seL4 microkernel, the first ever industrial-strength, general-purpose operating system with formally proved implementation correctness - using Isabelle!
-
Congratulations!
Katharina Kreuzer and Tobias Nipkow won the Best Student(-led) Paper at the Conference on Automated Deduction (CADE) 2023.
-
Congratulations!
Tobias Nipkow and Fabian Huch won the TeachInf Award for the best elective module in the winter term 2022/2023 at TUM.
-
Congratulations!
Our former team member Manuel Eberl has been awarded the “Schwärtzel-Dissertationspreis für Grundlagen der Informatik” for his Ph.D. thesis “Asymptotic Reasoning in a Proof Assistant”.
-
Congratulations!
Tobias Nipkow and Simon Roßkopf won the Best Paper Award at the Conference on Automated Deduction (CADE) 2021.
-
Congratulations!
Tobias Nipkow received the Herbrand Award 2021.
-
Free & Open-Source Software Course
Our course on Free & Open-Source Software is now free software! The course template is officially listed on the teaching open source website. The repository can be found here.
-
Congratulations!
Manuel Eberl and former Team member Peter Lammich teamed up and won the proving competition Proof Ground which happened alongside ITP 2019. See the results and problems of the morning and afternoon session.
-
Congratulations!
Manuel Eberl has received the “Distinguished Student Author Award” for his paper “Verified Real Asymptotics in Isabelle/HOL” at the International Symposium on Symbolic and Algebraic Computation 2019.
-
Congratulations!
Former Team member Fabian Immler has won the “Schwärtzel-Dissertationspreis für Grundlagen der Informatik” for his Ph.D. thesis “A Verified ODE Solver and Smale’s 14th Problem”.
-
Hilbert meets Isabelle
An Isabelle-formalization of Matiyasevich’s solution of Hilbert’s 10th problem won four prizes at the prestigeous German youth science competition “Jugend Forscht”. Congratulations! The project will be presented at the Isabelle Workshop 2018. (preprint paper)
-
Congratulations!
The team of Peter Lammich and Simon Wimmer have won the VerifyThis competition at ETAPS 2018. (Award Photograph)
-
The chair is co-organizing the 2017 Marktoberdorf SummerSchool. -
Congratulations!
Dmitriy Traytel has won the “Schwärtzel-Dissertationspreis für Grundlagen der Informatik” for his Ph.D. thesis “Formalizing Symbolic Decision Procedures for Regular Languages”.
-
Congratulations!
Dmitriy Traytel won the best student paper of FSCD 2016 with his paper Formal Languages, Formally and Coinductively.
-
Congratulations!
Jasmin C. Blanchette won the Best Paper Award at the International Joint Conference on Automated Reasoning (IJCAR) 2016.
-
Tom Hales and his collaborators finished the Flyspeck project, i.e., the formal proof of the Kepler conjecture with the help of the proof assistants HOL Light and Isabelle/HOL. Gertrud Bauer and Tobias Nipkow have contributed the Isabelle/HOL part of the proof. Flyspeck is the largest formal proof completed to date.
-
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). Congratulations 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!