Simon Wimmer

News

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.

Publications

Dissertation

• Trustworthy Verification of Realtime Systems
  Fakultät für Informatik, Technische Universiät München. December 2020.
  

Conference Papers

• Certifying Emptiness of Timed Büchi Automata.
  Simon Wimmer, Frédéric Herbreteau, and Jaco van de Pol. FORMATS 2020.
  The final publication is available at Springer Link.
  Slides.
• Verified Certification of Reachability Checking for Timed Automata.
  Simon Wimmer and Joshua von Mutius. TACAS 2020.
  The final publication is available at Springer Link.
• Munta: A Verified Model Checker for Timed Automata.
  Simon Wimmer. FORMATS 2019.
  The final publication is available at Springer Link.
  Slides.
• Verified Memoization and Dynamic Programming.
  Simon Wimmer, Shuwei Hu, and Tobias Nipkow. ITP 2018.
  The final publication is available at Springer Link.
  Slides. AFP entry.
• MDP + TA = PTA: Probabilistic Timed Automata, Formalized.
  Simon Wimmer and Johannes Hölzl. ITP 2018.
  The final publication is available at Springer Link.
  Slides. AFP entry.
• Verified Model Checking of Timed Automata.
  Simon Wimmer and Peter Lammich. TACAS 2018.
  The final publication is available at Springer Link.
  Supplementary material. Slides.
• Formalized Timed Automata.
  Simon Wimmer. ITP 2016.
  The final publication is available at Springer Link.

Workshop Papers

• Smashing Isabelle: Flex-Flex Pairs in 2016.
  Simon Wimmer. Isabelle Workshop 2016.
  

Posters

• Verified Model Checking of Timed Automata.
  Simon Wimmer and Peter Lammich. TABLEAUX/FroCoS/ITP 2017.
  

Archive of Formal Proofs

• Hidden Markov Models
  Simon Wimmer. May 2018.
  

• Probabilistic Timed Automata
  Simon Wimmer and Johannes Hölzl. May 2018.
  

• Monadification, Memoization and Dynamic Programming
  Simon Wimmer, Shuwei Hu and Tobias Nipkow. May 2018.
  

• VerifyThis 2018 – Polished Isabelle Solutions
  Peter Lammich and Simon Wimmer. April 2018.
  

• The Floyd-Warshall Algorithm for Shortest Paths
  Simon Wimmer and Peter Lammich. May 2017.
  

• Timed Automata
  Simon Wimmer. March 2016.
  

• Lehmer's Theorem
  Simon Wimmer and Lars Noschinski. July 2013.
  

• Pratt's Primality Certificates
  Simon Wimmer and Lars Noschinski. July 2013.
  

Bachelor's thesis

• Formally Verified Complexity Analysis of a Functional Language
  Institut für Informatik, Technische Universiät München. August 2014.
  

Tools