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 | Automated memory safety verification for unsafe Rust with separation logic | For languages such as Rust or C memory safety is key. Our research prototype tool BiFrust utilizes separation logic to automatically verify unsafe Rust code. As part of this project, many potential thesis topics are available. |
| 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. |