Sub Auspiciis Promotion
Marcel Moosbrugger received his doctorate sub auspiciis, a recognition for exceptional academic achievements, under the auspices of the Federal President of the Republic of Austria and the rectorate of TU Wien. Federal President Dr. Alexander Van der Bellen awarded Marcel Moosbrugger the Ring of Honor of the Republic of Austria in Hofburg on March 14. Marcel Moosbrugger’s Doctoral Thesis “Automated Analysis of Probabilistic Loops” was supervised by Laura Kovács and co-supervised by Ezio Bartocci.
Marcel Moosbrugger graduated as a Bachelor with Honors from TU Wien Informatics in 2019, and he he was a Distinguished Young Alumn Award winner in 2020. He received his Master’s Degree in 2020, and he won the Diploma Thesis Award of the City of Vienna in 2021. He was also nominated for the Austrian Master Thesis Prize and the Christiana Hörbiger Prize. During his studies, he supported eduLAB’s “Abenteuer Informatik” project, and he is currently working as an External Research Engineer at Huawei.
Dr. Moosbrugger’s Doctoral Thesis advanced the automated analysis of probabilistic loops by developing new theoretical and computational methods. It introduced a fully automated approach for computing higher moments of program variables using linear recurrences with constant coefficients, suitable for a broad class of probabilistic loops. This method was part of a new framework called the theory of moment-computable loops, which proved complete for programs incorporating branching, polynomial arithmetic, and varied probability distributions.
Additionally, a novel technique for automatic sensitivity analysis was developed to cater to probabilistic systems with unknown parameters, extending its application to non-moment-computable loops. The thesis also addressed the computational challenges in deriving polynomial invariants for probabilistic loops, identifying these problems as Skolem-hard. Despite these challenges, practical methods were proposed for computing bounded polynomial invariants and approximating polynomial loops with linearizable ones. The thesis presented Polar, a tool that implemented these techniques, demonstrating superior performance on complex benchmarks. It also introduced Amber, the first tool to certify both probabilistic termination and non-termination, highlighting significant theoretical and practical contributions to probabilistic program analysis.
