TY  - JOUR
PB  - ACM
UR  - https://doi.org/10.1145/3434320
ID  - discovery10115802
N2  - 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 ? to the expected value of f evaluated in the final states reached after termination C on ? (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 ? wp[C](f).
KW  - probabilistic programs
KW  -  randomized algorithms
KW  -  formal verification
KW  -  quantitative verification
KW  -  completeness
KW  -  weakest precondition
KW  -  weakest preexpectation
A1  - Batz, K
A1  - Kaminski, BL
A1  - Katoen, J-P
A1  - Matheja, C
JF  - Proceedings of the ACM on Programming Languages
AV  - public
Y1  - 2021/01//
VL  - 5
TI  - Relatively Complete Verification of Probabilistic Programs: An Expressive Language for Expectation-Based Reasoning
N1  - 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.
IS  - POPL
ER  -