conference paper published yes Mingzhang Huang author Hongfei Fu author Krishnendu Chatterjee author 2E5DCA20-F248-11E8-B48F-1D18A9856A870000-0002-4561-241X Amir Kafshdar Goharshady author 391365CE-F248-11E8-B48F-1D18A9856A870000-0003-1702-6584 KrCh department OOPSLA: Object-oriented Programming, Systems, Languages and Applications Efficient Algorithms for Computer Aided Verification project Game Theory project Quantitative Graph Games: Theory and Applications project Quantitative Analysis of Probabilistic Systems with a focus on Crypto-Currencies project Quantitative Game-theoretic Analysis of Blockchain Applications and Smart Contracts project In this work, we consider the almost-sure termination problem for probabilistic programs that asks whether a given probabilistic program terminates with probability 1. Scalable approaches for program analysis often rely on modularity as their theoretical basis. In non-probabilistic programs, the classical variant rule (V-rule) of Floyd-Hoare logic provides the foundation for modular analysis. Extension of this rule to almost-sure termination of probabilistic programs is quite tricky, and a probabilistic variant was proposed in [16]. While the proposed probabilistic variant cautiously addresses the key issue of integrability, we show that the proposed modular rule is still not sound for almost-sure termination of probabilistic programs. Besides establishing unsoundness of the previous rule, our contributions are as follows: First, we present a sound modular rule for almost-sure termination of probabilistic programs. Our approach is based on a novel notion of descent supermartingales. Second, for algorithmic approaches, we consider descent supermartingales that are linear and show that they can be synthesized in polynomial time. Finally, we present experimental results on a variety of benchmarks and several natural examples that model various types of nested while loops in probabilistic programs and demonstrate that our approach is able to efficiently prove their almost-sure termination property https://research-explorer.ista.ac.at/download/6780/6807/oopsla-2019.pdf application/pdfno https://research-explorer.ista.ac.at/download/6780/7821/2019_ACM_Huang.pdf application/pdfno ACM2019Athens, Greece eng 1901.0608710.1145/3360555 3 https://research-explorer.ista.ac.at/record/8934 Huang, M., Fu, H., Chatterjee, K., &#38; Goharshady, A. K. (2019). Modular verification for almost-sure termination of probabilistic programs. In <i>Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications </i> (Vol. 3). Athens, Greece: ACM. <a href="https://doi.org/10.1145/3360555">https://doi.org/10.1145/3360555</a> M. Huang, H. Fu, K. Chatterjee, A.K. Goharshady, in:, Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications , ACM, 2019. Huang, Mingzhang, et al. “Modular Verification for Almost-Sure Termination of Probabilistic Programs.” <i>Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications </i>, vol. 3, 129, ACM, 2019, doi:<a href="https://doi.org/10.1145/3360555">10.1145/3360555</a>. M. Huang, H. Fu, K. Chatterjee, and A. K. Goharshady, “Modular verification for almost-sure termination of probabilistic programs,” in <i>Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications </i>, Athens, Greece, 2019, vol. 3. Huang, Mingzhang, Hongfei Fu, Krishnendu Chatterjee, and Amir Kafshdar Goharshady. “Modular Verification for Almost-Sure Termination of Probabilistic Programs.” In <i>Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications </i>, Vol. 3. ACM, 2019. <a href="https://doi.org/10.1145/3360555">https://doi.org/10.1145/3360555</a>. Huang M, Fu H, Chatterjee K, Goharshady AK. Modular verification for almost-sure termination of probabilistic programs. In: <i>Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications </i>. Vol 3. ACM; 2019. doi:<a href="https://doi.org/10.1145/3360555">10.1145/3360555</a> Huang M, Fu H, Chatterjee K, Goharshady AK. 2019. Modular verification for almost-sure termination of probabilistic programs. Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications . OOPSLA: Object-oriented Programming, Systems, Languages and Applications vol. 3, 129. 67802019-08-09T09:54:20Z2026-09-13T22:31:00Z