@article{discovery10115802,
            note = {This is an open access article under the CC BY license (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.},
          volume = {5},
          number = {POPL},
           month = {January},
         journal = {Proceedings of the ACM on Programming Languages},
           title = {Relatively Complete Verification of Probabilistic Programs: An Expressive Language for Expectation-Based Reasoning},
            year = {2021},
       publisher = {ACM},
        keywords = {probabilistic programs, randomized algorithms, formal verification, quantitative verification, completeness, weakest precondition, weakest preexpectation},
          author = {Batz, K and Kaminski, BL and Katoen, J-P and Matheja, C},
        abstract = {We study a syntax for specifying quantitative "assertions" - functions mapping program states to numbers - for probabilistic program verification. We prove that our syntax is expressive in the following sense: Given any probabilistic program C, if a function f is expressible in our syntax, then the function mapping each initial state {\ensuremath{\sigma}} to the expected value of f evaluated in the final states reached after termination C on {\ensuremath{\sigma}} (also called the weakest preexpectation wp[C](f)) is also expressible in our syntax. As a consequence, we obtain a relatively complete verification system for verifying expected values and probabilities in the sense of Cook: Apart from a single reasoning step about the inequality of two functions given as syntactic expressions in our language, given f, g, and C, we can check whether g {$\leq$} wp[C](f).},
             url = {https://doi.org/10.1145/3434320}
}