--- res: bibo_abstract: - 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. Like others, 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 classical results on denumerable (non-demonic) Markov chains.@eng bibo_authorlist: - foaf_Person: foaf_givenName: Annabelle foaf_name: Mciver, Annabelle foaf_surname: Mciver - foaf_Person: foaf_givenName: Carroll foaf_name: Morgan, Carroll foaf_surname: Morgan - foaf_Person: foaf_givenName: Benjamin Lucien foaf_name: Kaminski, Benjamin Lucien foaf_surname: Kaminski - foaf_Person: foaf_givenName: Joost P foaf_name: Katoen, Joost P foaf_surname: Katoen foaf_workInfoHomepage: http://www.librecat.org/personId=4524F760-F248-11E8-B48F-1D18A9856A87 bibo_doi: 10.1145/3158121 bibo_issue: POPL bibo_volume: 2 dct_date: 2017^xs_gYear dct_isPartOf: - http://id.crossref.org/issn/2475-1421 dct_language: eng dct_publisher: Association for Computing Machinery@ dct_title: A new proof rule for almost-sure termination@ ...