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

Probabilistic programs extend classical imperative programs with real-valued random variables and random branching. The most basic liveness property for such programs is the termination property. The qualitative (aka almost-sure) termination problem given a probabilistic program asks whether the program terminates with probability~1. While ranking functions provide a sound and complete method for non-probabilistic programs, the extension of them to probabilistic programs is achieved via ranking supermartingales (RSMs). While deep theoretical results have been established about RSMs, their application to probabilistic programs with nondeterminism has been limited only to academic examples. For non-probabilistic programs, lexicographic ranking functions provide a compositional and practical approach for termination analysis of real-world programs. In this work we introduce lexicographic RSMs and show that they present a sound method for almost-sure termination of probabilistic programs with nondeterminism. We show that lexicographic RSMs provide a tool for compositional reasoning about almost-sure termination, and for probabilistic programs with linear arithmetic they can be synthesized efficiently (in polynomial time). We also show that with additional restrictions even asymptotic bounds on expected termination time can be obtained through lexicographic RSMs. Finally, we present experimental results on abstractions of real-world programs to demonstrate the effectiveness of our approach.

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