Robbert Krebbers

Teaching

I am currently teaching the following course:

In the past, I have taught the following courses:

Master thesis projects

I am looking for master students to work on Coq, formal semantics, program verification, compiler verification, program logics, semantics of Rust and C, etc. Below, I have included a list of suggestions, but feel free to contact me with your own ideas.

Verified compilation of inline assembly in C

High-performance software, like operating systems, cryptographic algorithms, big number libraries, network protocols, file systems, make use of inline assembly to hand-optimize pieces of code that are executed often. In your master project you will develop a formal semantics for inline assembly.

A possible starting point is the CompCert compiler, an optimizing C compiler that has been written and verified entirely in the Coq proof assistant. You will extend the semantics of CompCert's source C language with support for inline assembly, and extend the compiler correctness proofs to show that the semantics of inline assembly is preserved.

Formal semantics of the C preprocessor

Most programs written in C and C++ make use of the C preprocessor, a macro language to transform programs before compilation. A typical use of the C preprocessor is to replaces macro with their definitions or to include and exclude pieces of code depending on the configuration. Although there has been a lot of work on formal semantics of C (see Section 10 of my PhD thesis for an overview of work in this area), there has not been any work on the semantics of the C preprocessor.

The goal of your master thesis is to develop a formal semantics of the C preprocessor. On top of that, you should investigate how to use the C preprocessor semantics to carry out proofs of macros, or proofs of programs that are parametric in their configuration.

Reasoning about programs with I/O

Most current tools and logics for program verification are limited to proving partial program correctness using Hoare triples. A Hoare triple { P } s { Q } states that that if the pre-condition P holds on the initial state, then the program s will not crash, and when it terminates, the final state will satisfy the post-condition Q.

Unfortunately, there is a significant shortcoming here: for most actual programs, the end-result is not necessarily of interest (some programs, like your operating system or window manager, typically do not even terminate). Instead, one mostly cares about I/O, for example, the way the program interacts with system resources like the operating system, file-system or network.

The goal of your master thesis is to extend state-of-the-art tools or logics to support reasoning about I/O. A possible direction is to extend the Iris framework for concurrent separation logic in the Coq proof assistant.

Verification of concurrent algorithms

It is very difficult to write bug-free fine-grained concurrent algorithms (e.g. algorithms that make use of low-level primitives like compare and swap). Over the last ten years there has been a lot of progress on program logics based on concurrent separation logic that allow one to establish that algorithms behave as expected for all possible inputs and under all possible executions.

In order to use concurrent separation logic to verify bigger and more complicated concurrent algorithms one needs a tool to helps constructing the proofs, and to verify that the proofs are mathematically valid. Iris is a modern framework in the Coq proof assistant for concurrent separation logic.

This list below contains some suggestions for your master thesis:

Prove coherence of traits in Rust

The Rust programming languages uses a concept called traits to provide ad-hoc polymorphism. A typical example is operator overloading. For example, the trait Eq is used to overload the behavior of the == operator depending on the type of its arguments, and the trait Hash is used to register the hash function of each type.

A critical property for type safety of Rust is coherence of traits, which means that there is at most one instance of each trait for each type. This property is easily satisfied when the language does not allow for overlap of traits at all, but for practical purposes, there is a need to permit overlap in some cases.

In your master thesis you will develop a formal semantics of traits in Rust using the Coq proof assistant and prove coherence of traits. Next, you will extend your formalization with one or more proposed extensions of the trait machinery (for example, those discussed here) and prove coherence.