SPLASH 2023
Sun 22 - Fri 27 October 2023 Cascais, Portugal
Wed 25 Oct 2023 16:36 - 16:54 at Room I - probabilistic Chair(s): Chandrakana Nandi

We present a new proof rule for verifying lower bounds on quantities of probabilistic programs. Our proof rule is not confined to almost-surely terminating programs – as is the case for existing rules – and can be used to establish non-trivial lower bounds on, e.g., termination probabilities and expected values, for possibly divergent probabilistic loops, e.g., the well-known three-dimensional random walk on a lattice.

Wed 25 Oct

Displayed time zone: Lisbon change

16:00 - 17:30
probabilisticOOPSLA at Room I
Chair(s): Chandrakana Nandi Certora
16:00
18m
Talk
A Deductive Verification Infrastructure for Probabilistic Programs
OOPSLA
Philipp Schröer RWTH Aachen University, Kevin Batz RWTH Aachen University, Benjamin Lucien Kaminski Saarland University; University College London, Joost-Pieter Katoen RWTH Aachen University, Christoph Matheja DTU
DOI
16:18
18m
Talk
A Gradual Probabilistic Lambda Calculus
OOPSLA
Wenjia Ye University of Hong Kong, Matías Toro University of Chile, Federico Olmedo University of Chile
DOI
16:36
18m
Talk
Lower Bounds for Possibly Divergent Probabilistic Programs
OOPSLA
Shenghua Feng Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Mingshuai Chen Zhejiang University, Han Su Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Benjamin Lucien Kaminski Saarland University; University College London, Joost-Pieter Katoen RWTH Aachen University, Naijun Zhan Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences
Link to publication DOI Pre-print
16:54
18m
Talk
Exact Recursive Probabilistic Programming
OOPSLA
David Chiang University of Notre Dame, Colin McDonald University of Notre Dame, Chung-chieh Shan Indiana University
DOI
17:12
18m
Talk
Solving String Constraints with Lengths by StabilizationDistinguished Paper
OOPSLA
Yu-Fang Chen Academia Sinica, David Chocholatý Brno University of Technology, Vojtěch Havlena Brno University of Technology, Lukáš Holík Brno University of Technology, Ondřej Lengál Brno University of Technology, Juraj Síč Brno University of Technology
DOI