Alexandra Graß

I'm a PhD student in Theoretical Computer Science and Theorem Proving at LMU Munich under the supervision of Jasmin Blanchette. I am also a member of Helmut Seidl's group for Formal Languages, Compiler Construction, Software Construction at Technical University of Munich, and the DFG Research Training Group ConVeY.

My research focuses on the formalization of algorithms and datastructures used at the core of safety-critical software. I am currently mechanizing egg, an e-graph-based framework for building program optimizers and synthesizers based on equality saturation. Previous projects focused on the formal verification of a fixpoint engine at the heart of Goblint, a static analysis tool for multi-threaded C programs and based on abstract interpretation. I mainly work with the interactive theorem prover Isabelle, although I also have some experience with Lean.

You can send me email at <my first name>.<my last name>@ifi.lmu.de, where the letter ß is replaced by ss.

My office is room D 012, Oettingenstraße 67.

Publications

  • Proving Total Correctness of Top-Down Solvers with Widening and Narrowing. Sarah Tilscher, Alexandra Graß, Helmut Seidl, Yannick Stade. Journal of Automated Reasoning 70, article number 15, 2026. Publisher's page
  • Verifying a Solver for Mixed Flow-Sensitive Analyses. Sarah Tilscher, Alexandra Graß, Helmut Seidl. In Havelund, K., Pinto, A. (eds.) NASA Formal Methods (18th International Symposium, NFM 2026), LNCS 16622, pp. 48–69, Springer, 2026. Publisher's page

Theses

  • Towards the Verification of Top-Down Solvers. Alexandra Graß. June 2024. Master's Thesis. Author's PDF
To top