How can we formally ensure that a program satisfies certain properties? For example, that it does not have memory bugs (such as null-pointer accesses, use-after-free, or buffer overflows) or concurrency bugs (such as data races or deadlocks), that it does not leak confidential information (such as passwords or personal information), or that its output adheres to some mathematical specification?
We we study two formalisms to prove such program properties:
- Types. Many programming languages classify program expressions using types, and thereby automatically rule out ill-behaved programs like `true + 10`. Modern programming languages like Rust use types to ensure that programs are free of much larger classes or bugs, like memory and concurrency bugs.
- Logic. Using logic one can specify and prove arbitrarily complicated properties of programs. To scale this up to imperative and concurrent programs, we study the formalism of concurrent separation logic (for which the inventors Brookes and O'Hearn received the 2016 Gödel price).
Typically we use proof assistants (like Coq) to implement and develop the theory of these formalisms. If you like logic, semantics, and functional programming, a bachelor or master project about these topics would be a good fit.
Below there are some directions for thesis topics.
The goal of this project is to apply an existing formalism to verify some algorithm, data structure, or program. For example, you could verify purely functional data structures using Coq, concurrent programs using the Iris tool that we developed, C programs using the RefinedC type system that we developed, or Rust program using the RustBelt framework.
It would be interesting to take code from real-life. For example, in collaboration with Google we are working on verifying the security and safety of a hypervisor, which involves lots of intriguing code that needs to be verified. Of course, you are allowed to verify a simplified version instead of (or before) verifying the real code.
The goal of this project is to develop a new formalism that supports a new program property, language feature, or kind of language semantics. For example, Edoardo Putti is currently developing a version of Incorrectness separation logic in the Coq proof assistant for his master student, and Liam Clark (external student at TU Delft) is extending Iris to support semantics based on interaction trees for his master thesis.
Prior knowledge of functional programming (e.g., NWI-IBC040 "Functional Programming") and semantics (e.g., NWI-IBC026 "Semantics and Correctness" and NWI-IBC025 "Semantics and Rewriting") is recommended. Having taken the course NWI-IMC010 "Type Theory and Coq" is beneficial for advanced master projects, but not a necessity.
In spring 2022 there will be a new master course called "Program verification with types and logic".
Contact Robbert Krebbers.