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

    Keywords

    • Probabilistic Programs
    • Symbolic Execution
    • Observe Statements
    • Continuous Distributions
    • SymProb Tool

    Fingerprint

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

    Cite this