Symbolic Semantics for Probabilistic Programs

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

doi:10.48550/arXiv.2307.09951

Symbolic Semantics for Probabilistic Programs

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

Computer Science

Research output: Conference Article in Proceeding or Book/Report chapter › Book chapter › Research › peer-review

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.

Original language	English
Title of host publication	Quantitative Evaluation of Systems 20th International Conference, QEST 2023, Antwerp, Belgium, September 20–22, 2023, Proceedings
Publisher	Springer, Cham
Publication date	2023
Pages	329-345
DOIs	https://doi.org/10.48550/arXiv.2307.09951
Publication status	Published - 2023
Event	Quantitative Evaluation of Systems - Duration: 20 Sept 2023 → … Conference number: 2023

Conference

Conference	Quantitative Evaluation of Systems
Number	2023
Period	20/09/2023 → …

Series	Lecture Notes in Computer Science
Number	QEST
Volume	14287
ISSN	0302-9743

Keywords

Probabilistic Programs
Symbolic Execution
Observe Statements
Continuous Distributions
SymProb Tool

Access to Document

10.48550/arXiv.2307.09951

https://arxiv.org/pdf/2307.09951.pdf

Cite this

@inbook{ddafa298f2f84a428ac91460b033560b,

title = "Symbolic Semantics for Probabilistic Programs",

abstract = "We present a new symbolic execution semantics of probabilistic programs that include observe statements and sampling from continuous distributions. Building on Kozen{\textquoteright}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.",

keywords = "Probabilistic Programs, Symbolic Execution, Observe Statements, Continuous Distributions, SymProb Tool, Probabilistic Programs, Symbolic Execution, Observe Statements, Continuous Distributions, SymProb Tool",

author = "Erik Voogd and {Broch Johnsen}, Einar and Alexandra Silva and Susag, {Zachary J.} and Andrzej Wasowski",

year = "2023",

doi = "10.48550/arXiv.2307.09951",

language = "English",

series = "Lecture Notes in Computer Science",

publisher = "Springer, Cham",

number = "QEST",

pages = "329--345",

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

note = "Quantitative Evaluation of Systems, QEST ; Conference date: 20-09-2023",

}

Voogd, E, Broch Johnsen, E, Silva, A, Susag, ZJ & Wasowski, A 2023, Symbolic Semantics for Probabilistic Programs. in Quantitative Evaluation of Systems 20th International Conference, QEST 2023, Antwerp, Belgium, September 20–22, 2023, Proceedings. Springer, Cham, Lecture Notes in Computer Science, no. QEST, vol. 14287, pp. 329-345, Quantitative Evaluation of Systems, 20/09/2023. https://doi.org/10.48550/arXiv.2307.09951

Symbolic Semantics for Probabilistic Programs. / Voogd, Erik; Broch Johnsen, Einar; Silva, Alexandra et al.
Quantitative Evaluation of Systems 20th International Conference, QEST 2023, Antwerp, Belgium, September 20–22, 2023, Proceedings. Springer, Cham, 2023. p. 329-345 (Lecture Notes in Computer Science; No. QEST, Vol. 14287).

Research output: Conference Article in Proceeding or Book/Report chapter › Book chapter › Research › peer-review

TY - CHAP

T1 - Symbolic Semantics for Probabilistic Programs

AU - Voogd, Erik

AU - Broch Johnsen, Einar

AU - Silva, Alexandra

AU - Susag, Zachary J.

AU - Wasowski, Andrzej

N1 - Conference code: 2023

PY - 2023

Y1 - 2023

N2 - 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.

AB - 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.

KW - Probabilistic Programs

KW - Symbolic Execution

KW - Observe Statements

KW - Continuous Distributions

KW - SymProb Tool

KW - Probabilistic Programs

KW - Symbolic Execution

KW - Observe Statements

KW - Continuous Distributions

KW - SymProb Tool

U2 - 10.48550/arXiv.2307.09951

DO - 10.48550/arXiv.2307.09951

M3 - Book chapter

T3 - Lecture Notes in Computer Science

SP - 329

EP - 345

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

PB - Springer, Cham

T2 - Quantitative Evaluation of Systems

Y2 - 20 September 2023

ER -

Symbolic Semantics for Probabilistic Programs

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this