probabilistic programs

A Unified Framework for Quantitative Analysis of Probabilistic Programs
Verifying probabilistic programs requires reasoning about various probabilistic behaviors, e.g., random sampling, nondeterminism, and …
PDF Cite DOI
A Unified Framework for Quantitative Analysis of Probabilistic Programs
Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions
We present an exact Bayesian inference method for inferring posterior distributions encoded by probabilistic programs featuring …
PDF Cite Artifact Evaluated
Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions
Latticed Craig Interpolation with an Application to Probabilistic Verification

In this work, we are primarily concerned with the question: Is Craig interpolation applicable to the automatic, quantitative …
PDF Cite
Latticed Craig Interpolation with an Application to Probabilistic Verification
Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants
Essential tasks for the verification of probabilistic programs include bounding expected outcomes and proving termination in finite …
PDF Cite DOI Artifact Evaluated
Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants
Lower Bounds for Possibly Divergent Probabilistic Programs
We present a new proof rule for verifying lower bounds on quantities of probabilistic programs. Our proof rule is not confined to …
PDF Cite Poster Slides DOI
Lower Bounds for Possibly Divergent Probabilistic Programs
Exact Probabilistic Inference Using Generating Functions
Probabilistic programs are typically normal-looking programs describing posterior probability distributions. They intrinsically code up …
PDF Cite Code
Exact Probabilistic Inference Using Generating Functions
Does a Program Yield the Right Distribution?
We study discrete probabilistic programs with potentially unbounded looping behaviors over an infinite state space. We present, to the …
PDF Cite DOI Artifact Evaluated
Does a Program Yield the Right Distribution?
Latticed $k$-Induction with an Application to Probabilistic Programs
We revisit two well-established verification techniques, $k$-induction and bounded model checking (BMC), in the more general setting of …
PDF Cite Slides DOI Artifact Evaluated Pulp Fiction
Latticed $k$-Induction with an Application to Probabilistic Programs
Latticed $k$-Induction and Probabilistic Programs

“Induction is a process of inference; it proceeds from the known to the unknown.”

– John S. Mill, 1806 – 1873
Apr 18, 2021
Latticed $k$-Induction and Probabilistic Programs