Symbolic Semantics for Probabilistic Programs (extended version)

TL;DR

This paper introduces a new symbolic execution semantics for probabilistic programs with continuous distributions and observe statements, enabling correctness proofs and implementation in a verification tool.

Contribution

It develops a novel symbolic semantics for probabilistic programs that includes continuous distributions and observe statements, extending prior work and enabling formal verification.

Findings

Correctness proof of symbolic execution for probabilistic programs

Implementation of the semantics in the symProb tool

Application to example 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'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.