If you are interested in writing a Bachelor’s or Master’s thesis in quantitative aspects of logic or verification, reach out to the person indicated with the topics below.

DIRECTIONS

Exploring Probabilistic Programming

Supervision: Tobias Gürtler

Probabilistic Programming Languages (PPLs) extend standard programming languages with statements to model random behaviour as well as statements to perform conditioning with observed evidence. This has allowed PPLs to make probabilistic modelling widely accessible to developers without much knowledge of probability theory. However, there are often many different ways to use probabilistic programs to model a system, and even deceptively similar looking programs can yield very different results.

The topic of this thesis is to explore such programs which are seemingly the same, but behave differently. As a starting point, different ways to model the Monty-Hall-Problem can be considered. Prior knowledge of PPLs is not necessary, but instead mathematical thinking and an interest in probabilistic modelling are needed.

Relating Kleene Algebra and Hoare Triples
Supervision: Lena Verscht

Kleene algebras with tests (KATs) are algebraic structures that can be used to reason about programs. A prominent example of this is a KAT equation expressing partial correctness, which roughly means that if a program terminates, then the reached final state satisfies a specified postcondition. There are numerous extensions of KATs, such as the addition of a top element to allow reasoning about incorrectness [1]. An alternative approach to characterising properties of programs is based on weakest precondition style transformers. Recently, a forward transformer has been introduced that is also capable of reasoning about incorrectness [2].

Possible concrete topics include investigating the relationships between KAT and Hoare triples in a probabilistic setting and exploring a language model of KAT in this context. You should like mathematics, ideally algebra. Experience with program analysis is also helpful.

[1] Cheng Zhang, Arthur Azevedo de Amorim, and Marco Gaboardi. 2022. On incorrectness logic and Kleene algebra with top and tests. Proc. ACM Program. Lang. 6, POPL, Article 29 (January 2022), 30 pages. https://doi.org/10.1145/3498690

[2] Linpeng Zhang and Benjamin Lucien Kaminski. 2022. Quantitative strongest post: a calculus for reasoning about the flow of quantitative information. Proc. ACM Program. Lang. 6, OOPSLA1, Article 87 (April 2022), 29 pages. https://doi.org/10.1145/3527331