Johannes Hölzl

36 papers A 3B 13Journal 15Unranked 4

Year	Rank	Type	Title / Venue / Authors
2024	J	`jnl`	AutoCorres2. Arch. Formal Proofs 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, Simon Wimmer
2022	—	`conf`	Towards a beneficial management of personal health records. CENTERIS/ProjMAN/HCist 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
2019	B	`conf`	Formalizing the Solution to the Cap Set Problem. ITP Sander R. Dahmen, Johannes Hölzl, Robert Y. Lewis
2019	J	`jnl`	Formalizing the Solution to the Cap Set Problem. CoRR Sander R. Dahmen, Johannes Hölzl, Robert Y. Lewis
2018	B	`conf`	MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper). ITP Simon Wimmer, Johannes Hölzl
2018	J	`jnl`	Probabilistic Timed Automata. Arch. Formal Proofs Simon Wimmer, Johannes Hölzl
2017	J	`jnl`	A Formally Verified Proof of the Central Limit Theorem. J. Autom. Reason. Jeremy Avigad, Johannes Hölzl, Luke Serafin
2017	J	`jnl`	A Verified Compiler for Probability Density Functions. CoRR Manuel Eberl, Johannes Hölzl, Tobias Nipkow
2017	—	`conf`	Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic. FroCoS Julian Biendarra, Jasmin Christian Blanchette, Aymeric Bouzy, Martin Desharnais, Mathias Fleury, Johannes Hölzl, Ondrej Kuncar, Andreas Lochbihler, Fabian Meier, Lorenz Panny, Andrei Popescu, Christian Sternagel, René Thiemann, Dmitriy Traytel
2017	J	`jnl`	Markov Chains and Markov Decision Processes in Isabelle/HOL. J. Autom. Reason. Johannes Hölzl
2017	B	`conf`	Markov processes in Isabelle/HOL. CPP Johannes Hölzl
2016	B	`conf`	Formalising Semantics for Expected Running Time of Probabilistic Programs. ITP Johannes Hölzl
2015	B	`conf`	A Formalized Hierarchy of Probabilistic System Types - Proof Pearl. ITP Johannes Hölzl, Andreas Lochbihler, Dmitriy Traytel
2015	A	`conf`	A Verified Compiler for Probability Density Functions. ESOP Manuel Eberl, Johannes Hölzl, Tobias Nipkow
2015	J	`jnl`	A Zoo of Probabilistic Systems. Arch. Formal Proofs Johannes Hölzl, Andreas Lochbihler, Dmitriy Traytel
2015	J	`jnl`	Verification of the UpDown Scheme. Arch. Formal Proofs Johannes Hölzl
2014	J	`jnl`	A Verified Compiler for Probability Density Functions. Arch. Formal Proofs Manuel Eberl, Johannes Hölzl, Tobias Nipkow
2014	J	`jnl`	A formally verified proof of the Central Limit Theorem. CoRR Jeremy Avigad, Johannes Hölzl, Luke Serafin
2014	J	`jnl`	Probabilistic Noninterference. Arch. Formal Proofs Andrei Popescu, Johannes Hölzl
2014	B	`conf`	Recursive Functions on Lazy Lists via Domains and Topologies. ITP Andreas Lochbihler, Johannes Hölzl
2014	B	`conf`	Truly Modular (Co)datatypes for Isabelle/HOL. ITP Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, Dmitriy Traytel
2013	—	`—`	Construction and stochastic applications of measure spaces in higher-order logic. Johannes Hölzl
2013	J	`jnl`	Formal Verification of Language-Based Concurrent Noninterference. J. Formaliz. Reason. Andrei Popescu, Johannes Hölzl, Tobias Nipkow
2013	B	`conf`	Formalizing Probabilistic Noninterference. CPP Andrei Popescu, Johannes Hölzl, Tobias Nipkow
2013	B	`conf`	Noninterfering Schedulers - When Possibilistic Noninterference Implies Probabilistic Noninterference. CALCO Andrei Popescu, Johannes Hölzl, Tobias Nipkow
2013	B	`conf`	Type Classes and Filters for Mathematical Analysis in Isabelle/HOL. ITP Johannes Hölzl, Fabian Immler, Brian Huffman
2012	—	`conf`	Interactive verification of Markov chains: Two distributed protocol case studies QFM Johannes Hölzl, Tobias Nipkow
2012	J	`jnl`	Markov Models. Arch. Formal Proofs Johannes Hölzl, Tobias Nipkow
2012	B	`conf`	Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL. ITP Fabian Immler, Johannes Hölzl
2012	J	`jnl`	Ordinary Differential Equations. Arch. Formal Proofs Fabian Immler, Johannes Hölzl
2012	J	`jnl`	Possibilistic Noninterference. Arch. Formal Proofs Andrei Popescu, Johannes Hölzl
2012	B	`conf`	Proving Concurrent Noninterference. CPP Andrei Popescu, Johannes Hölzl, Tobias Nipkow
2012	A	`conf`	Verifying pCTL Model Checking. TACAS Johannes Hölzl, Tobias Nipkow
2011	B	`conf`	Three Chapters of Measure Theory in Isabelle/HOL. ITP Johannes Hölzl, Armin Heller
2010	—	`conf`	Quantitative Information Flow Analysis in Isabelle. AlgoSyn Johannes Hölzl
2010	A	`conf`	Specifying and verifying sparse matrix codes. ICFP Gilad Arnold, Johannes Hölzl, Ali Sinan Köksal, Rastislav Bodík, Mooly Sagiv