Thu 11 Jan 2018 13:40 - 14:05 at Bunker Hill - Termination Chair(s): Constantin Enea

We present a new proof rule for proving almost-sure termination of probabilistic programs, including those that contain demonic non-determinism. An important question for a probabilistic program is whether the probability mass of all its diverging runs is zero, that is that it terminates “almost surely”. Proving that can be hard, and this paper presents a new method for doing so. It applies directly to the program’s source code, even if the program contains demonic choice. We use variant functions (a.k.a. “super-martingales”) that are real-valued and decrease randomly on each loop iteration; but our key innovation is that the amount as well as the probability of the decrease are parametric. We prove the soundness of the new rule, indicate where its applicability goes beyond existing rules, and explain its connection to Blackwell’s classical results on denumerable (non-demonic) Markov chains.

Thu 11 Jan

Displayed time zone: Tijuana, Baja California change

13:40 - 15:20
TerminationResearch Papers at Bunker Hill
Chair(s): Constantin Enea Université Paris Diderot
13:40
25m
Talk
A new proof rule for almost-sure termination
Research Papers
Annabelle McIver Macquarie University, Carroll Morgan University of New South Wales; Data 61, Benjamin Lucien Kaminski RWTH Aachen University; University College London, Joost-Pieter Katoen RWTH Aachen University
14:05
25m
Talk
Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs
Research Papers
Sheshansh Agrawal IIT Bombay, Krishnendu Chatterjee IST Austria, Petr Novotný IST Austria
14:30
25m
Talk
Algorithmic Analysis of Termination Problems for Quantum Programs
Research Papers
Yangjia Li Institute of Software, Chinese Academy of Sciences, Mingsheng Ying University of Technology Sydney
14:55
25m
Talk
Monadic refinements for relational cost analysis
Research Papers
Ivan Radicek TU Vienna, Gilles Barthe IMDEA Software Institute, Marco Gaboardi University at Buffalo, SUNY, Deepak Garg Max Planck Institute for Software Systems, Florian Zuleger TU Vienna