Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL. - Alexander Schimpf; Stephan Merz; Jan-Georg Smaus (TPHOLs, 2009)

A Fully Verified Executable LTL Model Checker. - Javier Esparza; Peter Lammich; René Neumann; Tobias Nipkow; Alexander Schimpf; Jan-Georg Smaus (Arch. Formal Proofs, 2014)

Converting Linear-Time Temporal Logic to Generalized Büchi Automata. - Alexander Schimpf; Peter Lammich (Arch. Formal Proofs, 2014)

Büchi Automata Optimisations Formalised in Isabelle/HOL. - Alexander Schimpf; Jan-Georg Smaus (ICLA, 2015)

Eine vollständig verifizierte, ausführbare Formelübersetzung à la SPIN. - Alexander Schimpf (2015)