We supervise Bachelor's and Master's theses in verification, program analysis, logic, and automata theory. If one of the topics listed below interests you, please contact the corresponding supervisor.
| Supervisor | B/M | Title | Abstract |
| Pluska | B/M | ATP ablation | Modern ATP systems utilize a complex web of heuristics and optimizations, the impact of most is not cleanly ablated in literature. This thesis project consists of implementing a modern ATP feature in ProofAtlas and running an ablation study. |
| Sextl | B | Structured separation logic predicates | For languages such as Rust or C memory objects often have a tree-like shape with regard to fields, types, etc. However, many formalisms such as separation logic are defined in a more linear way. This topic aims to explore practically how the tree structure can be directly expressed in separation logic and how it affects the proof system. On main aspect of this topic is implementing the tree separation logic in our research prototype BiFrust. |
| Sextl | M | Biabduction for tree borrows | Rust's semantics are still work in progress. One such aspect is the aliasing model, where to date two approaches have been proposed. The more widely used model is Tree Borrows, and there is ongoing work on a separation logic for tree borrows. As such, one might ask whether it is also possible to define a biabduction procedure for the tree borrow separation logic to make reasoning about them fully automatic. |