Functional Binomial Queues. - René Neumann (Arch. Formal Proofs, 2010)

A Framework for Verified Depth-First Algorithms. - René Neumann (ATx/WInG@IJCAR, 2012)

Using Promela in a Fully Verified Executable LTL Model Checker. - René Neumann (VSTTE, 2014)

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

Promela Formalization. - René Neumann (Arch. Formal Proofs, 2014)

A Framework for Verifying Depth-First Search Algorithms. - Peter Lammich; René Neumann (Arch. Formal Proofs, 2016)

CAVA - A Verified Model Checker. - René Neumann (2017)