SPLASH 2022
Mon 5 - Sat 10 December 2022 Auckland, New Zealand
Fri 9 Dec 2022 16:00 - 16:30 at Seminar Room G007 - Probabilistic Chair(s): Benjamin Lucien Kaminski

We propose a symbolic execution method for programs that can draw random samples. In contrast to existing work, our method can verify randomized programs with unknown inputs and can prove probabilistic properties that universally quantify over all possible inputs. Our technique augments standard symbolic execution with a new class of \emph{probabilistic symbolic variables}, which represent the results of random draws, and computes symbolic expressions representing the probability of taking individual paths. We implement our method on top of the $KLEE$ symbolic execution engine alongside multiple optimizations, and use it to prove properties about probabilities and expected values for a range of challenging case studies written in C++, including Freivalds’ algorithm, randomized quicksort, and a randomized property-testing algorithm for monotonicity. We evaluate our method against $PSI$, an exact probabilistic symbolic inference engine, and $STORM$, a probabilistic model checker, and show that our method significantly outperforms both tools.

Fri 9 Dec

Displayed time zone: Auckland, Wellington change

15:30 - 17:00
ProbabilisticOOPSLA at Seminar Room G007
Chair(s): Benjamin Lucien Kaminski Saarland University and University College London
15:30
30m
Talk
Semi-symbolic Inference for Efficient Streaming Probabilistic Programming
OOPSLA
Eric Atkinson Massachusetts Institute of Technology, Charles Yuan Massachusetts Institute of Technology, Guillaume Baudart Inria, Louis Mandel IBM Research, Michael Carbin Massachusetts Institute of Technology
DOI
16:00
30m
Talk
Symbolic Execution for Randomized Programs
OOPSLA
Zachary Susag Cornell University, Sumit Lahiri IIT Kanpur, Justin Hsu Cornell University, Subhajit Roy IIT Kanpur
DOI
16:30
30m
Talk
This Is the Moment for Probabilistic Loops
OOPSLA
DOI