ABSTRACT. Program verification emerged in the late 1960s as a way to determine whether a program satisfies a given specification by translating the problem into a logical question. A decade later, model checking introduced the possibility of automating this verification process. Since the general verification problem is undecidable, early model-checking techniques focused on finite-state systems and propositional temporal properties, where automatic analysis is feasible.

ABSTRACT. For the past two years, I have been the Diversity Manager of the Faculty of Mathematics and Computer Science at the University of Bremen. In this talk, I will give an insight into my everyday work: supporting students in difficult situations, identifying barriers faced by people from diverse backgrounds, and developing measures to make faculty life more inclusive. I will also speak about our outreach activities, current challenges, and the small and large steps we take to improve participation, belonging, and equal opportunities in our faculty.

ABSTRACT. I will give a personally biased overview of projects in the space of interest for FLoC where proof assistants were used as more than proof checkers, covering amongst others results around Hilbert's tenth problem, the fifth busy beaver value, and computability. I will complement this by some general observations how to write up results of research projects involving proof assistants, trying to start an interactive discussion on how this differs to writing papers in general. I hope that the discussions scales to other tool use such as SAT or SMT solvers, and that the talk also sheds light on the question what makes a good research paper.

ABSTRACT. Privilege escalations are complex attack paths through which a user gains unintended access to a resource. The user chains together multiple operations—each one legitimate and authorized in isolation, such as creating new users; updating, attaching, or detaching policies; or assuming roles—until these assemble into a path that reaches a privilege they were never meant to have. At Huawei Cloud, we developed an SMT-based bounded model checking procedure that detects escalation paths of up to 5 steps, directly from a customer's account. Unsurprisingly, for large customers with thousands of deeply intertwined entities, the state space explodes as the search goes deeper. To make this scale, we applied sound state-space reductions. The soundness proof comes down to simulation, a well-known abstract technique I never expected to use at industrial scale. Thanks to this work, Huawei Cloud customers can now find 5-step privilege escalations in sub-second runtimes.

ABSTRACT. A lot of researchers struggle with finding their “next big idea,” and can get stuck waiting around until they see the whole path before starting anything new. In this talk, I’ll reflect on my own research journey (which started with automata theory and ended up spanning synthesis, networks, personalized education, and LLMs) and how many of the directions that shaped my work emerged not from following a fixed master plan, but from pursuing small ideas that gradually changed where I thought I was going. My goal is to share a perspective on how research directions actually develop in practice—and why consistently exploring and working through interesting questions often matters more than trying to predict the final destination from the start.

ABSTRACT. Career paths are shaped by a mix of deliberate choices, mistakes, and events beyond our control. In this talk, I reflect on decisions I believe I got right, choices I would make differently, and outcomes that unfolded regardless of intent — sometimes due to luck, sometimes to bad timing. Rather than presenting a recipe for success, the goal is to share concrete lessons about uncertainty, timing, and resilience, and to highlight what can (and cannot) be influenced along the way. I hope these reflections will help others navigate their own paths with more clarity, patience, and perspective.