Symbolic Semantics for Probabilistic Programs


We present a new symbolic execution semantics of probabilistic pro- grams that include observe statements and sampling from continuous distributions. Building on Kozen’s seminal work, this symbolic semantics consists of a countable collection of measurable functions, along with a partition of the state space. We use the new semantics to provide a full correctness proof of symbolic execution for probabilistic programs. We also implement this semantics in the tool symProb, and illustrate its use on examples.

Proc. 20th Intl. Conference on Quantitative Evaluation of SysTems (QEST 2023). LNCS 14287 © Springer 2023.
Erik Voogd
Erik Voogd
PhD Student