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