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.

Two typical examples from computer science and mathematics demonstrate the wide spectrum of possible applications of Isabelle:

The Kepler Conjecture says that the »cannonball packing« (see picture) is a densest packing of 3-dimensional balls of the same size. This was stated as a fact by Kepler in 1611 but only proved by Thomas Hales in 1998. His proof relies on a Java program for generating all (3000) possible counterexamples (all of which are then shown not to be counterexamples). With the help of Isabelle we were able to prove the correctness of a functional implementation of his Java program. Listen to Thomas Hales speaking about the proof (ABC Radio National Science Show, March 11th 2006). A formal proof of the Kepler conjecture was completed in 2014.

The Java Bytecode Verifier (JBV) is an essential part of the Java security architecture. It checks compiled Java programs ("bytecode") for well-formedness to prevent runtime errors (and thus potential attacks) like stack underflow or overflow. Despite its central role in the Java security architecture, for a long time the JBV was not well understood and its implementations by Sun and Microsoft contained security-critical bugs. Gerwin Klein was the first to formally verify a (functional) implementation of a bytecode verifier for Java. This won him the 2003 Dissertation Prize of the Gesellschaft für Informatik. Gerwin Klein then moved to NICTA where he co-lead the first-ever verification of an operating system kernel, the L4.verified project, again using Isabelle.

Current projects

[isabelle] Isabelle Generic interactive theorem proving
CAVA The CAVA Project Computer Aided Verification of Automata: a DFG-funded project, that formalises and verifies important algorithmic parts of automata theory and model checking using the proof assistant Isabelle/HOL.
[isabelle] Secure Type Systems and Deduction Verification of type systems for information flow analysis by combining interactive proofs in Isabelle/HOL with automatic proofs in SPASS
[PUMA] PUMA Program and Model Analysis
[isabelle] HOL-ML-Haskell Integrating Isabelle/HOL with the programming languages ML and Haskell

Past projects

[isabelle] Isar Intelligible semi-automated reasoning
[isabelle] Nominal Isabelle Nominal datatypes in Isabelle
[Flyspeck] Flyspeck The quest for a mechanically verified proof of the Kepler Conjecture
[esprit] TYPES Mathematical modelling and reasoning using typed logics.
[Verisoft] Verisoft Proving as an engineering science
[verypcc] VeryPCC Veryfied Proof-Carrying Code
GKLI DFG Graduiertenkolleg Logik in der Informatik
[inopsys] InopSys Interoperability of System Modeling Calculi
[verificard] VerifiCard Theorem proving for JavaCard
[bali] Bali Formalizing Java in Isabelle
[esprit] CCL Construction of Computational Logics. ESPRIT Working Group.
DEDUCTION Formal verification in Higher-Order Logic in Isabelle