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 Larry Paulson from the 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:

oranges 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).


Java logo 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.

Current projects

[isabelle] Isabelle Generic interactive theorem proving Partners:
Cambridge
[Flyspeck] Flyspeck The quest for a mechanically verified proof of the Kepler Conjecture Partners
[Verisoft] Verisoft Proving as an engineering science
PuMa Program and Model Analysis Partners
[verypcc] VeryPCC Veryfied Proof-Carrying Code
[isabelle] HOL-ML-Haskell Integrating Isabelle/HOL with the programming languages ML and Haskell
[isabelle] Isar Intelligible semi-automated reasoning
[esprit] TYPES Mathematical modelling and reasoning using typed logics. Partners
[isabelle] Nominal Isabelle Nominal datatypes in Isabelle

Past projects

[inopsys] InopSys Interoperability of System Modeling Calculi Partners:
Möller, Reif, Wirsing
[verificard] VerifiCard Theorem proving for JavaCard Partners:
Nijmegen, INRIA, Hagen, Sweden, Gemplus, Bull
[bali] Bali Formalizing Java in Isabelle
[esprit] CCL Construction of Computational Logics. ESPRIT Working Group.
DEDUCTION Formal verification in Higher-Order Logic in Isabelle