
@inproceedings{hoelzl2012verifyingpctl,
  title      = {Verifying {pCTL} Model Checking},
  author     = {Johannes H{\"o}lzl and Tobias Nipkow},
  year       = {2012},
  booktitle  = {Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012)},
  series     = {LNCS}
}

@inproceedings{hoelzl2012casestudies,
  author    = {H{\"o}lzl, Johannes and Nipkow, Tobias},
  title     = {Interactive verification of {Markov} chains: {Two} distributed protocol case studies},
  booktitle = {Quantities in Formal Methods (QFM 2012)},
  editor    = {Uli Fahrenberg and Axel Legay and Claus Thrane},
  doi       = {10.4204/EPTCS.103.2},
  year      = {2012},
  series    = {EPTCS},
  publisher = {arXiv},
  volume    = {103}
}

@inproceedings{hoelzl2016exprun,
  author    = {H{\"o}lzl, Johannes},
  editor    = {Blanchette, Jasmin Christian and Merz, Stephan},
  title     = {Formalising Semantics for Expected Running Time of Probabilistic Programs},
  booktitle = {Interactive Theorem Proving (ITP 2016)},
  year      = {2016},
  publisher = {Springer},
  pages     = {475--482},
  doi       = {10.1007/978-3-319-43144-4_30}
}

@inproceedings{hoelzl2017markovprocesses,
  author    = {Johannes H{\"{o}}lzl},
  title     = {Markov Processes in Isabelle/HOL},
  booktitle = {Certified Programs and Proofs (CPP 2017)},
  year      = {2017},
  editor    = {Yves Bertot and Viktor Vafeiadis},
  doi       = {10.1145/3018610.3018628},
  publisher = {ACM}
}

@article{hoelzl2017mdp,
  author     = {H{\"o}elzl Johannes},
  title      = {Markov chains and Markov decision processes in Isabelle/HOL},
  journal    = {Journal of Automated Reasoning},
  doi        = {10.1007/s10817-016-9401-5},
  year       = {2017},
  publisher  = {Springer}
}
