Projects for Students

We offer projects suitable for

The following projects are currently available.

Extending the Leon verification system with inductive predicates

Leon is a verification and synthesis toolkit for Scala programs, developed at EPFL. In recent work, Hupel and Kuncak have implemented a connection between Leon and Isabelle, i.e., Isabelle can be used to prove correctness of Scala programs. The goal of this thesis is to extend the Leon system with a mechanism to define inductive predicates and sets, and subsequently translate those to Isabelle.

Ein Testrahmen für funktionale Datenstrukturen

Es soll ein Testrahmen implementiert und ausgewertet werden, um die Effizienz funkionaler Datenstrukturen messen zu können. Dabei soll das Lastprofil, also der Mix der verschiedenen Operationen, flexibel spezifizierbar sein. Sodann sollen eine Reihe effizienter funktionaler Datenstrukturen für Suchbäume und Prioritätswarteschlangen implementiert und mit Hilfe dieses Testrahmens auf ihre Effizienz hin untersucht werden.

Efficient Graph-Algorithms in Isabelle/HOL

The goal of this master's thesis is to formalize some graph algorithm, e.g. the blossom algorithm for maximal cardinality matching, in Isabelle/HOL and use refinement techniques to refine the algorithm down to efficiently executable code.

Formalization of an imperative language with arrays and pointers

The goal of this master's thesis is to formalize a basic imperative language with pointers and arrays, and provide a proof infrastructure (e.g. Separation Logic) and/or a translation to a real imperative language (e.g. Java, C).

Pattern-based rewriting with congruence rules

Rewriting with conditional equations is one of the most important proof methods in Isabelle. When rewriting deep inside a term, we could use the knowledge about where we rewrite to discharge the conditions (e.g., if we rewrite in the left branch of an if expression, we can assume that the condition is true). This knowledge can be collected b using so-called congruence rules.

Numerical Proof Procedures in Isabelle/HOL

The Isabelle theorem prover can prove variable-free arithmetic statements automatically, for example arctan 1.5 < 1. The proof procedure uses Taylor polynomials and interval arithmetic. It should be extended to support more operations or make use of IEEE floating point numbers.

Multiple Precision Floating Point Arithmetic

Starting from the existing formalization of IEEE floating point numbers in the AFP, the goal of this thesis is to implement and verify a multiple precision floating point arithmetic library based on hardware floating point numbers in Isabelle/HOL.

Plotting Functions and Data within Isabelle's Document Preparation System

Various tools in the Isabelle theorem prover produce theorems involving numerical data, which would be best to visualize. When proving theorems about functions over the real numbers, the user might find it helpful to plot the functions involved. The aim of this thesis is to implement a facility to plot functions and numerical data using Isabelle's document preparation system, which translates Isabelle theories to LaTeX source.

Efficient Imperative Data Structures

Isabelle/Imperative-HOL ist eine einfache imperativ-funktionale Sprache in Isabelle/HOL. Ziel der Arbeit ist es eine einfache imperative Datenstruktur (Skip Lists oder Hash Maps) in Imperative-HOL zu implementieren und zu verifizieren.

Efficient Functional Data Structures

Mittels Codegenerierung können aus Spezifikationen unmittelbar Prototypen in einer funktionalen Programmiersprache erzeugt werden, z.B. in ML, in Haskell, oder in (einer Teilmenge von) Scala. Um die Effizienz dieser Prototypen zu steigern, sind effiziente Datenstrukturen erforderlich. Bekannte Beispiele hierfür sind balancierende Suchbäume (z.B. 2-3-Bäume); es gibt aber noch viel mehr Kandidaten. Eine Auswahl hiervon soll als Isabelle-Theorie implementiert und gegen eine naive Referenzimplementierung verifiziert werden.

Clone Detection in Isabelle Theories

Duplicate code segments, or “clones,” typically arise when developers simply copy & paste existing code to form the basis of new code. This practice complicates maintenance, because each bug fix in one such segment must normally be replicated in the other similar segments. The goal of this project is to develop a tool to detect clones in Isabelle theories. The tool should be developed as a frontend to an existing clone detection framework, such as ConQAT and JCCD.

SAT Solver in ML

SAT-Löser (SAT solvers) sind Programme, die erfüllende Belegungen für aussagenlogische Formeln berechnen. Ziel der Arbeit ist es, einen SAT Löser in (Standard) ML zu entwerfen und programmieren. (OCaml ist ein Dialekt von ML.) Dabei ist zu untersuchen, wie Implementierungstechniken von C sich auf ML übertragen lassen, wobei ML auch Arrays und Zeiger hat. Ausgangspunkt ist der in C geschriebene open source SAT-Löser MiniSat.

This list may be incomplete, and we are open to suggestions. If you have questions concerning a specific project, simply send an email to the project's supervisor. For general questions, contact Prof. Nipkow.