Simon Wimmer

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

I am a PostDoc at Aarhus University and a former PhD student in Tobias Nipkow's group at the Technical University of Munich. My research interests span various areas of formal methods. A big theme in my research is to increase the trustworthiness of model checkers with the help of proof assistants (usually Isabelle/HOL).

Mini Bio:

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


08.02.2021MSCA proposal for the project "Certywhere" accepted!

In the project, which was submitted with Jaco van de Pol, I aim towards the vision of "Certification Everywhere" (in model checking): I want to develop theory and verified certifiers for a large range of model checking techniques and formalisms, including partial-order reduction, symbolic model checking, and timed automata.

01.01.2021Started PostDoc at Aarhus University
I now work in the Logic and Semantics group under the supervision of Jaco van de Pol. Due to the pandemic you cannot find me in Aarhus yet.
07.12.2020PhD thesis successfully defended
02.09.2020Oded Maler best paper award at FORMATS 2020
With Jaco van de Pol and Frédéric Herbreteau, we won the Oded Maler best paper award at FORMATS 2020 for our paper Certifying Emptiness of Timed Büchi Automata.



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.