Simon Wimmer

Fakultät für Informatik · Boltzmannstr. 3 · 85748 Garching · Germany
Office: MI 00.09.064 · +49 (89) 289-17329 ·

I am a PhD student in Tobias Nipkow's group at the Technical University of Munich. My research interests evolve around algorithm verification with Isabelle/HOL and model checking of (probabilistic) timed automata.

Mini Bio:

  • B.Sc. Informatics @TUM ('11-'14)
  • MSE Computer and Information Science @University of Pennsylvania ('14-'15)
  • PhD student @TUM since Fall '15


Timed Automata

Verified Model Checking

I am constructing a model checker for the popular realtime-systems model formalism of timed automata. The clou is that the model checker's correctness is formally proved in Isabelle/HOL. For more information see our paper and the Github repository.

Fall 2015 - Present

Memoization & Dynamic Programming

Verified Memoization

We (Shuwei Hu, Tobias Nipkow, and me) are constructing a verified tool in Isabelle/HOL for the automatic memoization of verified functional programs. The functional programs can be used to describe dynamic programming algorithms. The memoization can target functional and imperative code. For more information see our paper and the AFP entry.

Summer 2017 - Present

Probabilistic Timed Automata

in Isabelle/HOL

We (Johannes Hölzl and me) are formalizing some foundational results on model checking of probabilistic timed automata in Isabelle/HOL. For more information see our paper and the AFP entry.

Fall 2015 - Present

Unification & Resolution

in Isabelle

We (Fabio Madge Pimentel and me) are working on the core resolution primitive in Isabelle's logical inference kernel. Its been around in its current form since the early days of Isabelle and still needs to trust an implementation of a complex higher-order unification algorithm due to Huet. Our goal is to instead certify unifiers for higher-order terms in the kernel, and to thus move the unification algorithm out of the trusted code base. Furthermore, we hope to facilitate experimentation with unification in Isabelle once the unification results do not have to be trusted anymore. For further information see my workshop paper.

Summer 2016 - Present


Conference Papers

Workshop Papers


Archive of Formal Proofs

Bachelor's thesis



Verified Model Checker for Timed Automata

See Github or try it here.

Unicode To Latex

Translation Tool

Paste some unicode text and see it converted to Latex. Uses common substitutions for Unicode characters with Latex symbols. Try it here.

Klima Hilbert

Climate Activism

See here.