| 2019 | ITP | Formalizing the Solution to the Cap Set Problem. | Sander R. Dahmen, Johannes Hlzl, Robert Y. Lewis |
| 2018 | ITP | MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper). | Simon Wimmer, Johannes Hlzl |
| 2017 | CPP | Markov processes in Isabelle/HOL. | Johannes Hlzl |
| 2016 | ITP | Formalising Semantics for Expected Running Time of Probabilistic Programs. | Johannes Hlzl |
| 2015 | ESOP | A Verified Compiler for Probability Density Functions. | Manuel Eberl, Johannes Hlzl, Tobias Nipkow |
| 2015 | ITP | A Formalized Hierarchy of Probabilistic System Types - Proof Pearl. | Johannes Hlzl, Andreas Lochbihler, Dmitriy Traytel |
| 2014 | ITP | Truly Modular (Co)datatypes for Isabelle/HOL. | Jasmin Christian Blanchette, Johannes Hlzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, Dmitriy Traytel |
| 2014 | ITP | Recursive Functions on Lazy Lists via Domains and Topologies. | Andreas Lochbihler, Johannes Hlzl |
| 2013 | CALCO | Noninterfering Schedulers - When Possibilistic Noninterference Implies Probabilistic Noninterference. | Andrei Popescu, Johannes Hlzl, Tobias Nipkow |
| 2013 | CPP | Formalizing Probabilistic Noninterference. | Andrei Popescu, Johannes Hlzl, Tobias Nipkow |
| 2013 | ITP | Type Classes and Filters for Mathematical Analysis in Isabelle/HOL. | Johannes Hlzl, Fabian Immler, Brian Huffman |
| 2012 | CPP | Proving Concurrent Noninterference. | Andrei Popescu, Johannes Hlzl, Tobias Nipkow |
| 2012 | ITP | Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL. | Fabian Immler, Johannes Hlzl |
| 2012 | TACAS | Verifying pCTL Model Checking. | Johannes Hlzl, Tobias Nipkow |
| 2011 | ITP | Three Chapters of Measure Theory in Isabelle/HOL. | Johannes Hlzl, Armin Heller |
| 2010 | ICFP | Specifying and verifying sparse matrix codes. | Gilad Arnold, Johannes Hlzl, Ali Sinan Kksal, Rastislav Bodk, Mooly Sagiv |