Dr. Johannes Hölzl <hoelzl@in.tum.de>

Chair for Logic and Verification

My interest is formalizing mathematics and verifying software in interactive theorem provers. Since April 2019, I work as a Formal Verification Engineer at Apple.

Google Scholar - ORCID - DBLP - GitHub @johoelzl - Bitbucket @johannes2011 - Twitter @johannes2007

I studied computer science, with mathematics as minor subject, at the TU München since 2004. From May 2009 until October 2012 I was a graduate student as part of the PUMA graduate school. From 2013 until January 2017 I was working on the DFG project Ni/491 15-1. From February 2017 to October 2017 I was at CMU's Department of Philosophy with Jeremy Avigad. Working with the Lean Theorem Prover. Afterwards, I joined Jasmin Blanchette's team at the VU. There I worked on Matryoshka and later Lean Forward.

Wir müssen wissen,
wir werden wissen. - David Hilbert

Publications

Journal Articles

• A formally verified proof of the Central Limit Theorem (Preprint).
  Jeremy Avigad, Johannes Hölzl, and Luke Serafin.
  Submitted for review to the Journal of Automated Reasoning. arxiv (1405.7012)
• Markov chains and Markov decision processes in Isabelle/HOL (Preprint).
  Johannes Hölzl.
  Accepted for publication in the Journal of Automated Reasoning. BibTex Slides
  (The original publication is available at Springer Link)
• Formal Verification of Language-Based Concurrent Noninterference.
  Andrei Popescu, Johannes Hölzl, and Tobias Nipkow.
  Journal of Formalized Reasoning 6(1), 2013. BibTex

Conference Proceedings

• Markov Processes in Isabelle/HOL.
  Johannes Hölzl.
  Proceedings of CPP '17. BibTex
  ©Johannes Hölzl 2017. This is the author's version of the work. It is posted here for your personal use. Not for redistribution. The definitive version was published in the proceedings of CPP 2017.
• Formalising Semantics for Expected Running Time of Probabilistic Programs (Rough Diamond).
  Johannes Hölzl.
  Proceedings of ITP '16. BibTex Slides
  (The original publication is available at Springer Link)
• A Formalized Hierarchy of Probabilistic System Types - Proof Pearl.
  Johannes Hölzl, Andreas Lochbihler, and Dmitriy Traytel.
  Proceedings of ITP '15 (LNCS 9236). BibTex Slides
  (The original publication is available at Springer Link)
• A Verified Compiler for Probability Density Functions.
  Manuel Eberl, Johannes Hölzl, and Tobias Nipkow.
  Proceedings of ESOP '15. (LNCS 9032) BibTex
  (The original publication is available at Springer Link)
• Recursive Functions on Lazy Lists via Domains and Topologies.
  Andreas Lochbihler and Johannes Hölzl.
  Proceedings of ITP '14 (LNCS 8558). BibTex
  (The original publication is available at Springer Link)
• Truly Modular (Co)datatypes for Isabelle/HOL.
  Jasmin C. Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, and Dmitriy Traytel.
  Proceedings of ITP '14 (LNCS 8558). BibTex
  (The original publication is available at Springer Link)
• Formalizing Probabilistic Noninterference.
  Andrei Popescu, Johannes Hölzl, and Tobias Nipkow.
  Proceedings of CPP 2013 (LNCS 8307). BibTex
  (The original publication is available at Springer Link)
• Noninterfering Schedulers - When Possibilistic Noninterference Implies Probabilistic Noninterference.
  Andrei Popescu, Johannes Hölzl, and Tobias Nipkow.
  Proceedings of CALCO 2013 (LNCS 8089). BibTex
  (The original publication is available at Springer Link)
• Type Classes and Filters for Mathematical Analysis in Isabelle/HOL.
  Johannes Hölzl, Fabian Immler, and Brian Huffman.
  Proceedings of ITP '13 (LNCS 7998). BibTex
  (The original publication is available at Springer Link)
• Proving concurrent noninterference.
  Andrei Popescu, Johannes Hölzl, and Tobias Nipkow.
  Proceedings of CPP '12 (LNCS 7679). BibTex
  (The original publication is available at Springer Link)
• Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL.
  Fabian Immler and Johannes Hölzl.
  Proceedings of ITP '12 (LNCS 7406). BibTex
  (The original publication is available at Springer Link)
• Verifying pCTL Model Checking.
  Johannes Hölzl and Tobias Nipkow.
  Proceedings of TACAS '12 (LNCS 7214). BibTex
  (The original publication is available at Springer Link)
• Three Chapters of Measure Theory.
  Johannes Hölzl and Armin Heller.
  Proceedings of ITP '11 (LNCS 6898). BibTex
  (The original publication is available at Springer Link)
• Specifying and Verifying Sparse Matrix Codes.
  Gilad Arnold, Johannes Hölzl, Ali Sinan Köksal, Rastislav Bodík, and Mooly Sagiv.
  Proceedings of ICFP '10. (© ACM) BibTex
• Proving Inequalities over Reals with Computation in Isabelle/HOL.
  Johannes Hölzl.
  Proceedings of PLMMS '09. (© ACM) Slides BibTex

Workshops

• Fixed Points for Markov Decision Processes.
  Johannes Hölzl.
  Poster presentation at the Workshop on Probabilistic Programming Semantics (PPS2016)
• A formally verified proof of the Central Limit Theorem.
  Jeremy Avigad, Johannes Hölzl and Luke Serafin.
  Published at arXiv. Presented at the Isabelle Workshop 2014. bibTex
• Interactive verification of Markov chains: Two distributed protocol case studies.
  Johannes Hölzl and Tobias Nipkow.
  Proceedings of QFM '12 (EPTCS 103). Slides bibTex

Thesis

• Construction and Stochastic Applications of Measure Spaces in Higher-Order Logic.
  Institut für Informatik, TU München. October 2012. BibTex

Diploma thesis

• Proving Real-Valued Inequalities by Computation in Isabelle/HOL.
  Diploma thesis. Institut für Informatik, TU München. April 2009. BibTex

Current Work

Verification of probabilistic models in the interactive theorem prover Isabelle/HOL

I'm working on the DFG project Ni 491/15-1 and Ni 491/16-1.

Past Work

Measure, Probability, and Information

Together with Armin Heller I formalized the first three chapters of Heinz Bauer's textbook about measure theory. This is now officially part of the Isabelle repository. We built on the work from Aaron Coble which was ported to Isabelle by Lawrence C. Paulson. This work is now largely rewritten and extended, for an overview see my thesis and the work on the Giry monad, on Markov models, on the central limit theorem (CTL), and on Markov processes.

Multivariate Analysis

Robert Himmelmann ported large parts of the formalization of Multivariate Analysis available in HOL Light. The current development is found in the Isabelle repository.

Up Down

I'm working together with Dirk Pflüger on the publication of the verification of the up-down algorithm.

Verification of Sparse Matrix codes

Gilad Arnold and I are working on automatically verifying the correctness of Sparse Matrix codes.

Diploma thesis

Proving Real-Valued Inequalities by Computation in Isabelle/HOL

SEP

Developing Isabelle user interface components for interactive Prover-IDEs based on jEdit. This is the origin of isabelle-jedit.

IDP

Verifying the up-down algorithm