🎓 Thesis defended!

On October 1st, I successfully defended my PhD thesis “Automatically Analyzing Termination and Expected Runtime Complexity of Probabilistic Term Rewriting” at RWTH Aachen University, and I am very happy to say that it was awarded with distinction! 🎉

Probabilistic programs, i.e., programs that can make random choices during execution, are important in many applications, but randomness introduces new challenges for formal verification. In my thesis, I developed techniques for fully automatic termination and expected runtime complexity analysis of probabilistic term rewrite systems (PTRSs). Since programs in languages like Java, C, Haskell, and Prolog can be automatically transformed into term rewrite systems, these approaches have broad applications.

Some highlights of my dissertation:

• The annotated dependency pair framework: a modular divide-and-conquer framework and the most powerful automated technique for proving termination and upper bounds of expected runtime analysis of PTRSs up to now.
• Techniques to disprove termination, i.e., finding bugs instead of proving their absence, by embedding non-terminating random walks into rewrite sequences.
• The first composability and modularity results, as well as the first decision procedures for termination of non-trivial subclasses of PTRSs.

All these techniques have been implemented in our open source tool AProVE: https://aprove.informatik.rwth-aachen.de/

Thanks to everyone in the research group “Programming Languages and Verification”, the MOVES and Theory of Hybrid Systems groups, the UnRAVeL Research Training Group, everyone from the rewriting community, and everyone I met during all the conferences and summer schools for making these years so much fun!

#PhD #PhDDefense #RWTHAachen #FormalMethods #AutomatedReasoning #ProbabilisticPrograms #Termination #TermRewriting