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 OctDisplayed time zone: Lisbon change
Wed 25 Oct
Displayed time zone: Lisbon change
16:00 - 17:30 | |||
16:00 18mTalk | 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 18mTalk | 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 18mTalk | 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 18mTalk | 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 18mTalk | Solving String Constraints with Lengths by Stabilization 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 |