Voogd, E;
Johnsen, EB;
Silva, A;
Susag, ZJ;
Wąsowski, A;
(2023)
Symbolic Semantics for Probabilistic Programs.
In:
International Conference on Quantitative Evaluation of Systems QEST 2023: Quantitative Evaluation of Systems.
(pp. pp. 329-345).
Springer, Cham
Preview |
PDF
2307.09951.pdf - Accepted Version Download (614kB) | Preview |
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.
| Type: | Proceedings paper |
|---|---|
| Title: | Symbolic Semantics for Probabilistic Programs |
| Event: | Quantitative Evaluation of Systems 20th International Conference, QEST 2023 |
| ISBN-13: | 9783031438349 |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1007/978-3-031-43835-6_23 |
| Publisher version: | https://doi.org/10.1007/978-3-031-43835-6_23 |
| Language: | English |
| Additional information: | This version is the author accepted manuscript. For information on re-use, please refer to the publisher’s terms and conditions. |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/10182020 |
Archive Staff Only
 |
View Item |
