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

13:40 - 15:20: Research Papers - Termination at Bunker Hill
Chair(s): Constantin EneaUniversité Paris Diderot
POPL-2018-papers13:40 - 14:05
Annabelle McIverMacquarie University, Carroll MorganUniversity of New South Wales; Data 61, Benjamin Lucien KaminskiRWTH Aachen University; University College London, Joost-Pieter KatoenRWTH Aachen University
POPL-2018-papers14:05 - 14:30
Sheshansh AgrawalIIT Bombay, Krishnendu ChatterjeeIST Austria, Petr NovotnyIST Austria
POPL-2018-papers14:30 - 14:55
Yangjia LiInstitute of Software, Chinese Academy of Sciences, Mingsheng YingUniversity of Technology Sydney
POPL-2018-papers14:55 - 15:20
Ivan RadicekTU Vienna, Gilles BartheIMDEA Software Institute, Marco GaboardiUniversity at Buffalo, SUNY, Deepak GargMax Planck Institute for Software Systems, Florian ZulegerTU Vienna