Symbolic Semantics for Probabilistic Programs (extended version)
Programming Languages
2023-07-20 v1
Abstract
We present a new symbolic execution semantics of probabilistic programs 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.
Cite
@article{arxiv.2307.09951,
title = {Symbolic Semantics for Probabilistic Programs (extended version)},
author = {Erik Voogd and Einar Broch Johnsen and Alexandra Silva and Zachary J. Susag and Andrzej Wąsowski},
journal= {arXiv preprint arXiv:2307.09951},
year = {2023}
}
Comments
38 pages including references and appendices, 14 pages excluding, accepted at QEST'23, to appear in LNCS, Springer