h1

% IMPORTANT: The following is UTF-8 encoded.  This means that in the presence
% of non-ASCII characters, it will not work with BibTeX 0.99 or older.
% Instead, you should use an up-to-date BibTeX implementation like “bibtex8” or
% “biber”.

@PHDTHESIS{Kaminski:755408,
      author       = {Kaminski, Benjamin Lucien},
      othercontributors = {Katoen, Joost-Pieter and McIver, Annabelle},
      title        = {{A}dvanced weakest precondition calculi for probabilistic
                      programs},
      school       = {RWTH Aachen University},
      type         = {Dissertation},
      address      = {Aachen},
      reportid     = {RWTH-2019-01829},
      pages        = {1 Online-Ressource (xiv, 363 Seiten) : Illustrationen,
                      Diagramme},
      year         = {2019},
      note         = {Veröffentlicht auf dem Publikationsserver der RWTH Aachen
                      University; Dissertation, RWTH Aachen University, 2019},
      abstract     = {We study quantitative reasoning about probabilistic
                      programs. In doing so, we investigate two main aspects: The
                      reasoning techniques themselves and the computational
                      hardness of that reasoning. As for the former aspect, we
                      first give a comprehensive introduction to weakest
                      preexpectation reasoning à la McIver $\&$ Morgan - a
                      reasoning technique for the verification of probabilistic
                      programs that builds on Dijkstra's weakest precondition
                      calculus for programs with nondeterminism and Kozen's
                      probabilistic propositional dynamic logic for probabilistic
                      programs. We then develop advanced
                      weakest-preexpectation-style calculi for probabilistic
                      programs that enable reasoning about - expected runtimes, -
                      conditional expected values and conditional probabilities,
                      and - expected values of mixed-sign random variables. As
                      with Dijkstra's calculus, our calculi are defined
                      inductively on the program structure and thus allow for
                      compositional reasoning on source code level. We put a
                      special emphasis on proof rules for reasoning about loops.
                      The second aspect we study is the inherent computational
                      hardness of reasoning about probabilistic programs, which is
                      independent from the employed analysis technique. In
                      particular, we study the hardness of approximating expected
                      values and (co)variances. We show that lower bounds on
                      expected values are not computable but computably
                      enumerable, whereas upper bounds are not computably
                      enumerable. For covariances, we show that neither lower nor
                      upper bounds are computably enumerable. Furthermore, we
                      study the hardness of deciding termination of probabilistic
                      programs. While we study different notions of probabilistic
                      termination, for instance almost-sure termination or
                      termination within finite expected time (also known as
                      positive almost-sure termination), we show that deciding
                      termination of probabilistic programs is generally strictly
                      harder than deciding termination of nonprobabilistic
                      programs.},
      cin          = {121310 / 080060 / 120000},
      ddc          = {004},
      cid          = {$I:(DE-82)121310_20140620$ / $I:(DE-82)080060_20170720$ /
                      $I:(DE-82)120000_20140620$},
      pnm          = {FRAPPANT - Formal Reasoning About Probabilistic Programs:
                      Breaking New Ground for Automation (787914)},
      pid          = {G:(EU-Grant)787914},
      typ          = {PUB:(DE-HGF)11},
      doi          = {10.18154/RWTH-2019-01829},
      url          = {https://publications.rwth-aachen.de/record/755408},
}