Symbolic Semantics for Probabilistic Programs

Erik Voogd
,
Einar Broch Johnsen
,
Alexandra Silva
,
Zachary J. Susag
,
Andrzej Wasowski

University of Oslo
,
Cornell University

Research Output:

Conference Article in Proceeding or Book/Report chapter

Book chapter

Peer-review

Open access

Publication Information

Output type

Research Output:

Conference Article in Proceeding or Book/Report chapter

Book chapter

Peer-review

Original language

English

Pages from-to (Number of pages)

Pages 329-345

Publication milestones

Published - 2023

Publication status

Published - 2023

Publisher

Springer, United States, Germany

Book series

Book series name: Lecture Notes in Computer Science
Series number: QEST
Volume: 14287
ISSN: 0302-9743

Publication IDs

Scopus: 85174271638

Host publication title

Quantitative Evaluation of Systems 20th International Conference, QEST 2023, Antwerp, Belgium, September 20–22, 2023, Proceedings

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.