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