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

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