--- res: bibo_abstract: - "In this work, we consider the almost-sure termination problem for probabilistic programs that asks whether a\r\ngiven probabilistic program terminates with probability 1. Scalable approaches for program analysis often\r\nrely on modularity as their theoretical basis. In non-probabilistic programs, the classical variant rule (V-rule)\r\nof Floyd-Hoare logic provides the foundation for modular analysis. Extension of this rule to almost-sure\r\ntermination of probabilistic programs is quite tricky, and a probabilistic variant was proposed in [16]. While the\r\nproposed probabilistic variant cautiously addresses the key issue of integrability, we show that the proposed\r\nmodular rule is still not sound for almost-sure termination of probabilistic programs.\r\nBesides establishing unsoundness of the previous rule, our contributions are as follows: First, we present a\r\nsound modular rule for almost-sure termination of probabilistic programs. Our approach is based on a novel\r\nnotion of descent supermartingales. Second, for algorithmic approaches, we consider descent supermartingales\r\nthat are linear and show that they can be synthesized in polynomial time. Finally, we present experimental\r\nresults on a variety of benchmarks and several natural examples that model various types of nested while\r\nloops in probabilistic programs and demonstrate that our approach is able to efficiently prove their almost-sure\r\ntermination property@eng" bibo_authorlist: - foaf_Person: foaf_givenName: Mingzhang foaf_name: Huang, Mingzhang foaf_surname: Huang - foaf_Person: foaf_givenName: Hongfei foaf_name: Fu, Hongfei foaf_surname: Fu - foaf_Person: foaf_givenName: Krishnendu foaf_name: Chatterjee, Krishnendu foaf_surname: Chatterjee foaf_workInfoHomepage: http://www.librecat.org/personId=2E5DCA20-F248-11E8-B48F-1D18A9856A87 orcid: 0000-0002-4561-241X - foaf_Person: foaf_givenName: Amir Kafshdar foaf_name: Goharshady, Amir Kafshdar foaf_surname: Goharshady foaf_workInfoHomepage: http://www.librecat.org/personId=391365CE-F248-11E8-B48F-1D18A9856A87 orcid: 0000-0003-1702-6584 bibo_doi: 10.1145/3360555 bibo_volume: 3 dct_date: 2019^xs_gYear dct_language: eng dct_publisher: ACM@ dct_title: Modular verification for almost-sure termination of probabilistic programs@ ...