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 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:
- 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 email directly to any other member of the team.

The chair is actively involved in co-organizing the Marktoberdorf Summer School.

### News

- 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.
**We moved offices, our chair is now in corridor 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!