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 proving 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

The Isabelle logo Isabelle Generic interactive theorem proving
The Isabelle logo SW_GruVe Verified Proof Term Checking for Isabelle
robot ConVeY DFG Research Training Group “Continuous Verification of Cyber-Physical Systems”
automaton 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.
Verified Algorithm Analysis Reinhart Koselleck Project

Past projects

The Isabelle logo 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
The PUMA logo PUMA DFG Research Training Group “Program and Model Analysis”
Quis Custodiet Quis Custodiet DFG Project “Semantic Modelling, Analysis and Verification of Language-Based Software Security”
The Isabelle HOL-EXEC logo HOL-ML-Haskell Integrating Isabelle/HOL with the programming languages ML and Haskell
The Isabelle/Isar logo Isar Intelligible semi-automated reasoning
The Nominal Isabelle logo Nominal Isabelle Nominal datatypes in Isabelle
Flyspeck Flyspeck The quest for a mechanically verified proof of the Kepler Conjecture
The ESPRIT logo TYPES Mathematical modelling and reasoning using typed logics.
The Verisoft logo Verisoft Proving as an engineering science
The Isabelle/VeryPCC logo VeryPCC Veryfied Proof-Carrying Code
The logo of the Deutsche Forschungsgemeinschaft (DFG) GKLI DFG Research Training Group “Logik in der Informatik”
The InopSys logo InopSys Interoperability of System Modeling Calculi
The VerifiCard logo VerifiCard Theorem proving for JavaCard
[bali] Bali Formalizing Java in Isabelle
The ESPRIT logo CCL Construction of Computational Logics. ESPRIT Working Group.
The Isabelle/HOL logo DEDUCTION Formal verification in Higher-Order Logic in Isabelle