Quantitative Information Flow Analysis in Isabelle. - Johannes Hölzl (AlgoSyn, 2010)

Specifying and verifying sparse matrix codes. - Gilad Arnold; Johannes Hölzl; Ali Sinan Köksal; Rastislav Bodík; Mooly Sagiv (ICFP, 2010)

Three Chapters of Measure Theory in Isabelle/HOL. - Johannes Hölzl; Armin Heller (ITP, 2011)

Proving Concurrent Noninterference. - Andrei Popescu 001; Johannes Hölzl; Tobias Nipkow (CPP, 2012)

Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL. - Fabian Immler; Johannes Hölzl (ITP, 2012)

Verifying pCTL Model Checking. - Johannes Hölzl; Tobias Nipkow (TACAS, 2012)

Markov Models. - Johannes Hölzl; Tobias Nipkow (Arch. Formal Proofs, 2012)

Ordinary Differential Equations. - Fabian Immler; Johannes Hölzl (Arch. Formal Proofs, 2012)

Possibilistic Noninterference. - Andrei Popescu 001; Johannes Hölzl (Arch. Formal Proofs, 2012)

Interactive verification of Markov chains: Two distributed protocol case studies - Johannes Hölzl; Tobias Nipkow (QFM, 2012)

Noninterfering Schedulers - When Possibilistic Noninterference Implies Probabilistic Noninterference. - Andrei Popescu 001; Johannes Hölzl; Tobias Nipkow (CALCO, 2013)

Formalizing Probabilistic Noninterference. - Andrei Popescu 001; Johannes Hölzl; Tobias Nipkow (CPP, 2013)

Type Classes and Filters for Mathematical Analysis in Isabelle/HOL. - Johannes Hölzl; Fabian Immler; Brian Huffman (ITP, 2013)

Formal Verification of Language-Based Concurrent Noninterference. - Andrei Popescu 001; Johannes Hölzl; Tobias Nipkow (J. Formaliz. Reason., 2013)

Construction and stochastic applications of measure spaces in higher-order logic. - Johannes Hölzl (2013)

Truly Modular (Co)datatypes for Isabelle/HOL. - Jasmin Christian Blanchette; Johannes Hölzl; Andreas Lochbihler; Lorenz Panny; Andrei Popescu 001; Dmitriy Traytel (ITP, 2014)

Recursive Functions on Lazy Lists via Domains and Topologies. - Andreas Lochbihler; Johannes Hölzl (ITP, 2014)

Probabilistic Noninterference. - Andrei Popescu 001; Johannes Hölzl (Arch. Formal Proofs, 2014)

A Verified Compiler for Probability Density Functions. - Manuel Eberl; Johannes Hölzl; Tobias Nipkow (ESOP, 2015)

A Formalized Hierarchy of Probabilistic System Types - Proof Pearl. - Johannes Hölzl; Andreas Lochbihler; Dmitriy Traytel (ITP, 2015)

Verification of the UpDown Scheme. - Johannes Hölzl (Arch. Formal Proofs, 2015)

A Zoo of Probabilistic Systems. - Johannes Hölzl; Andreas Lochbihler; Dmitriy Traytel (Arch. Formal Proofs, 2015)

Formalising Semantics for Expected Running Time of Probabilistic Programs. - Johannes Hölzl (ITP, 2016)

Markov processes in Isabelle/HOL. - Johannes Hölzl (CPP, 2017)

Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic. - Julian Biendarra; Jasmin Christian Blanchette; Aymeric Bouzy; Martin Desharnais; Mathias Fleury; Johannes Hölzl; Ondrej Kuncar; Andreas Lochbihler; Fabian Meier; Lorenz Panny; Andrei Popescu 001; Christian Sternagel; et al. (FroCoS, 2017)

A Formally Verified Proof of the Central Limit Theorem. - Jeremy Avigad; Johannes Hölzl; Luke Serafin (J. Autom. Reason., 2017)

Markov Chains and Markov Decision Processes in Isabelle/HOL. - Johannes Hölzl (J. Autom. Reason., 2017)

MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper). - Simon Wimmer 001; Johannes Hölzl (ITP, 2018)

Probabilistic Timed Automata. - Simon Wimmer 001; Johannes Hölzl (Arch. Formal Proofs, 2018)

Formalizing the Solution to the Cap Set Problem. - Sander R. Dahmen; Johannes Hölzl; Robert Y. Lewis (ITP, 2019)

Towards a beneficial management of personal health records. - Christian Kop; Gerhard Leitner; Peter Schartner; Volodymyr A. Shekhovtsov; Claudia Steinberger; Eleni Zografou; Daniela Elisabeth Ströckl; Christoph Voutsinas; Herbert Groiss; Johannes Hölzl; Markus Irrasch (CENTERIS/ProjMAN/HCist, 2022)

AutoCorres2. - Matthew Brecknell; David Greenaway; Johannes Hölzl; Fabian Immler; Gerwin Klein; Rafal Kolanski; Japheth Lim; Michael Norrish; Norbert Schirmer; Salomon Sickert; Thomas Sewell; Harvey Tuch; et al. (Arch. Formal Proofs, 2024)