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

Publikation: Konference artikel i Proceeding eller bog/rapport kapitel › Bidrag til bog/antologi › Forskning › 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.

Originalsprog	Engelsk
Titel	Quantitative Evaluation of Systems 20th International Conference, QEST 2023, Antwerp, Belgium, September 20–22, 2023, Proceedings
Forlag	Springer, Cham
Publikationsdato	2023
Sider	329-345
DOI	https://doi.org/10.48550/arXiv.2307.09951
Status	Udgivet - 2023
Begivenhed	Quantitative Evaluation of Systems - Varighed: 20 sep. 2023 → … Konferencens nummer: 2023

Konference

Konference	Quantitative Evaluation of Systems
Nummer	2023
Periode	20/09/2023 → …

Navn	Lecture Notes in Computer Science
Nummer	QEST
Vol/bind	14287
ISSN	0302-9743

Adgang til dokumentet

10.48550/arXiv.2307.09951

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

Citationsformater

@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",

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. i Quantitative Evaluation of Systems 20th International Conference, QEST 2023, Antwerp, Belgium, September 20–22, 2023, Proceedings. Springer, Cham, Lecture Notes in Computer Science, nr. QEST, bind 14287, s. 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. s. 329-345 (Lecture Notes in Computer Science; Nr. QEST, Bind 14287).

Publikation: Konference artikel i Proceeding eller bog/rapport kapitel › Bidrag til bog/antologi › Forskning › 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

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

Konference

Adgang til dokumentet

Fingeraftryk

Citationsformater