Symbolic Semantics for Probabilistic Programs

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

Research output: Conference Article in Proceeding or Book/Report chapterBook chapterResearchpeer-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 languageEnglish
Title of host publication Quantitative Evaluation of Systems 20th International Conference, QEST 2023, Antwerp, Belgium, September 20–22, 2023, Proceedings
PublisherSpringer, Cham
Publication date2023
Pages329-345
DOIs
Publication statusPublished - 2023
EventQuantitative Evaluation of Systems -
Duration: 20 Sept 2023 → …
Conference number: 2023

Conference

ConferenceQuantitative Evaluation of Systems
Number2023
Period20/09/2023 → …
SeriesLecture Notes in Computer Science
NumberQEST
Volume14287
ISSN0302-9743

Fingerprint

Dive into the research topics of 'Symbolic Semantics for Probabilistic Programs'. Together they form a unique fingerprint.

Cite this