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”.

@MASTERSTHESIS{Schroer:998370,
      author       = {Schroer, Philipp},
      othercontributors = {Katoen, Joost-Pieter and Müller, Peter and Batz, Kevin and
                          Kaminski, Benjamin and Matheja, Christoph},
      title        = {{A} deductive verifier for probabilistic programs},
      school       = {RWTH Aachen University},
      type         = {Masterarbeit},
      address      = {Aachen},
      publisher    = {RWTH Aachen University},
      reportid     = {RWTH-2024-11340},
      pages        = {1 Online-Ressource: Illustrationen},
      year         = {2024},
      note         = {Veröffentlicht auf dem Publikationsserver der RWTH Aachen
                      University 2024; Masterarbeit, RWTH Aachen University, 2022},
      abstract     = {We design and implement a deductive verification
                      infrastructure for probabilistic programs. It consists of a
                      quantitative intermediate verification language (HeyVL) and
                      a quantitative assertion language (HeyLo). HeyLo is a syntax
                      to express expected values of probabilistic programs, with
                      support for quantitative implications based on Gödel logic.
                      Both HeyLo and HeyVL contain lattice-theoretic dual
                      constructs to reason about lower and upper bounds of
                      expected values. As a case study, we encode weakest
                      pre-expectation and weakest liberal pre-expectation
                      reasoning about the probabilistic programming language pGCL
                      into HeyVL. For loops, we provide encodings of Park
                      induction, k-induction, and bounded model checking. Park
                      induction and k-induction are both proof rules that require
                      on user-provided invariant candidates. Furthermore, we
                      discuss the automation of our deductive verification
                      infrastructure. Our implementation Caesar takes a HeyVL
                      program as input, generates and optimizes verification
                      conditions in the form of HeyLo formulas and uses the
                      automated theorem prover Z3 to prove or disprove validity of
                      the verification conditions. In this thesis, we focus on the
                      central optimization of quantifier elimination of HeyLo
                      formulas. We present early promising experimental results.
                      Finally, we discuss the abstraction of our framework based
                      on Heyting and Gödel algebras to support more domains than
                      expectations.},
      cin          = {121310 / 120000},
      ddc          = {004},
      cid          = {$I:(DE-82)121310_20140620$ / $I:(DE-82)120000_20140620$},
      typ          = {PUB:(DE-HGF)19},
      doi          = {10.18154/RWTH-2024-11340},
      url          = {https://publications.rwth-aachen.de/record/998370},
}