{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,21]],"date-time":"2026-07-21T23:03:40Z","timestamp":1784675020490,"version":"3.55.0"},"reference-count":46,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T00:00:00Z","timestamp":1576800000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"crossref","award":["61802254,61672229,61832015,61772336,11871221"],"award-info":[{"award-number":["61802254,61672229,61832015,61772336,11871221"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Austrian Science Fund (FWF) NFN","award":["S11407-N23 (RiSE\/SHiNE)"],"award-info":[{"award-number":["S11407-N23 (RiSE\/SHiNE)"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2020,1]]},"abstract":"<jats:p>The notion of program sensitivity (aka Lipschitz continuity) specifies that changes in the program input result in proportional changes to the program output. For probabilistic programs the notion is naturally extended to expected sensitivity. A previous approach develops a relational program logic framework for proving expected sensitivity of probabilistic while loops, where the number of iterations is fixed and bounded. In this work, we consider probabilistic while loops where the number of iterations is not fixed, but randomized and depends on the initial input values. We present a sound approach for proving expected sensitivity of such programs. Our sound approach is martingale-based and can be automated through existing martingale-synthesis algorithms. Furthermore, our approach is compositional for sequential composition of while loops under a mild side condition. We demonstrate the effectiveness of our approach on several classical examples from Gambler's Ruin, stochastic hybrid systems and stochastic gradient descent. We also present experimental results showing that our automated approach can handle various probabilistic programs in the literature.<\/jats:p>","DOI":"10.1145\/3371093","type":"journal-article","created":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T19:45:25Z","timestamp":1576871125000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["Proving expected sensitivity of probabilistic programs with randomized variable-dependent termination time"],"prefix":"10.1145","volume":"4","author":[{"given":"Peixin","family":"Wang","sequence":"first","affiliation":[{"name":"Shanghai Jiao Tong University, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Hongfei","family":"Fu","sequence":"additional","affiliation":[{"name":"Shanghai Jiao Tong University, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Krishnendu","family":"Chatterjee","sequence":"additional","affiliation":[{"name":"IST Austria, Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yuxin","family":"Deng","sequence":"additional","affiliation":[{"name":"East China Normal University, China \/ Pengcheng Laboratory, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ming","family":"Xu","sequence":"additional","affiliation":[{"name":"East China Normal University, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,12,20]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.3166\/ejc.16.624-641"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158122"},{"key":"e_1_2_2_3_1","volume-title":"Joost-Pieter Katoen, and Christoph Matheja.","author":"Aguirre Alejandro","year":"2019","unstructured":"Alejandro Aguirre , Gilles Barthe , Justin Hsu , Benjamin Lucien Kaminski , Joost-Pieter Katoen, and Christoph Matheja. 2019 . Kantorovich Continuity of Probabilistic Programs. CoRR abs\/1901.06540 (2019). arXiv: 1901.06540 http:\/\/arxiv.org\/abs\/ 1901.06540 Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. 2019. Kantorovich Continuity of Probabilistic Programs. CoRR abs\/1901.06540 (2019). arXiv: 1901.06540 http:\/\/arxiv.org\/abs\/ 1901.06540"},{"key":"e_1_2_2_4_1","volume-title":"Random walks on finite groups and rapidly mixing Markov chains. S\u00e9minaire de probabilit\u00e9s de Strasbourg 17","author":"Aldous David J.","year":"1983","unstructured":"David J. Aldous . 1983. Random walks on finite groups and rapidly mixing Markov chains. S\u00e9minaire de probabilit\u00e9s de Strasbourg 17 ( 1983 ), 243\u2013297. http:\/\/www.numdam.org\/item\/SPS_1983__17__243_0 David J. Aldous. 1983. Random walks on finite groups and rapidly mixing Markov chains. S\u00e9minaire de probabilit\u00e9s de Strasbourg 17 (1983), 243\u2013297. http:\/\/www.numdam.org\/item\/SPS_1983__17__243_0"},{"key":"e_1_2_2_5_1","first-page":"912","article-title":"Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model","volume":"2016","author":"Barthe Gilles","year":"2016","unstructured":"Gilles Barthe , Fran\u00e7ois Dupressoir , Sebastian Faust , Benjamin Gr\u00e9goire , Fran\u00e7ois-Xavier Standaert , and Pierre-Yves Strub . 2016 . Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model . IACR Cryptology ePrint Archive 2016 (2016), 912 . http:\/\/eprint.iacr.org\/2016\/912 Gilles Barthe, Fran\u00e7ois Dupressoir, Sebastian Faust, Benjamin Gr\u00e9goire, Fran\u00e7ois-Xavier Standaert, and Pierre-Yves Strub. 2016. Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model. IACR Cryptology ePrint Archive 2016 (2016), 912. http:\/\/eprint.iacr.org\/2016\/912","journal-title":"IACR Cryptology ePrint Archive"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158145"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480894"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009896"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103670"},{"key":"e_1_2_2_10_1","volume-title":"Probability and Measure","author":"Billingsley Patrick","unstructured":"Patrick Billingsley . 1995. Probability and Measure . JOHN WILEY &amp; SONS. Patrick Billingsley. 1995. Probability and Measure. JOHN WILEY &amp; SONS."},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1162\/153244302760200704"},{"key":"e_1_2_2_12_1","volume-title":"Probabilistic Program Analysis with Martingales. In CAV","author":"Chakarov Aleksandar","year":"2013","unstructured":"Aleksandar Chakarov and Sriram Sankaranarayanan . 2013 . Probabilistic Program Analysis with Martingales. In CAV 2013. 511\u2013526. Aleksandar Chakarov and Sriram Sankaranarayanan. 2013. Probabilistic Program Analysis with Martingales. In CAV 2013. 511\u2013526."},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28729-9_18"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_1"},{"key":"e_1_2_2_15_1","volume-title":"Computational Approaches for Stochastic Shortest Path on Succinct MDPs. In IJCAI","author":"Chatterjee Krishnendu","year":"2018","unstructured":"Krishnendu Chatterjee , Hongfei Fu , Amir Kafshdar Goharshady , and Nastaran Okati . 2018 a. Computational Approaches for Stochastic Shortest Path on Succinct MDPs. In IJCAI 2018. 4700\u20134707. Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady, and Nastaran Okati. 2018a. Computational Approaches for Stochastic Shortest Path on Succinct MDPs. In IJCAI 2018. 4700\u20134707."},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2018\/653"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3174800"},{"key":"e_1_2_2_18_1","volume-title":"POPL","author":"Chatterjee Krishnendu","year":"2017","unstructured":"Krishnendu Chatterjee , Petr Novotn\u00fd , and \u00d0or\u0111e \u017dikeli\u0107. 2017. Stochastic invariants for probabilistic termination . In POPL 2017 . 145\u2013160. Krishnendu Chatterjee, Petr Novotn\u00fd, and \u00d0or\u0111e \u017dikeli\u0107. 2017. Stochastic invariants for probabilistic termination. In POPL 2017. 145\u2013160."},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706308"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009890"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2003.09.013"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/11681878_14"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1561\/0400000042"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2015.2424951"},{"key":"e_1_2_2_25_1","volume-title":"A Fourier-f\u00e9le mechanikai elv alkalmaz\u00e1sai (Hungarian). Mathematikai\u00e9s Term\u00e9szettudom\u00e1nyi \u00c9rtesit\u00f6 12","author":"Farkas J.","year":"1894","unstructured":"J. Farkas . 1894. A Fourier-f\u00e9le mechanikai elv alkalmaz\u00e1sai (Hungarian). Mathematikai\u00e9s Term\u00e9szettudom\u00e1nyi \u00c9rtesit\u00f6 12 ( 1894 ), 457\u2013472. J. Farkas. 1894. A Fourier-f\u00e9le mechanikai elv alkalmaz\u00e1sai (Hungarian). Mathematikai\u00e9s Term\u00e9szettudom\u00e1nyi \u00c9rtesit\u00f6 12 (1894), 457\u2013472."},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-68167-2_26"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31585-5_23"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-11245-5_22"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429113"},{"key":"e_1_2_2_30_1","volume-title":"Proceedings of the 33nd International Conference on Machine Learning, ICML 2016","author":"Hardt Moritz","year":"2016","unstructured":"Moritz Hardt , Ben Recht , and Yoram Singer . 2016 . Train faster, generalize better: Stability of stochastic gradient descent . In Proceedings of the 33nd International Conference on Machine Learning, ICML 2016 , New York City, NY, USA , June 19-24, 2016. 1225\u20131234. http:\/\/jmlr.org\/proceedings\/papers\/v48\/hardt16.html Moritz Hardt, Ben Recht, and Yoram Singer. 2016. Train faster, generalize better: Stability of stochastic gradient descent. In Proceedings of the 33nd International Conference on Machine Learning, ICML 2016, New York City, NY, USA, June 19-24, 2016. 1225\u20131234. http:\/\/jmlr.org\/proceedings\/papers\/v48\/hardt16.html"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-02768-1_11"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-01090-4_23"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_15"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(85)90012-1"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49213-5_14"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158121"},{"key":"e_1_2_2_37_1","doi-asserted-by":"crossref","unstructured":"S.P. Meyn and R.L. Tweedie. 1993. Markov Chains and Stochastic Stability. Springer-Verlag London. available at: probability.ca\/MT.  S.P. Meyn and R.L. Tweedie. 1993. Markov Chains and Stochastic Stability. Springer-Verlag London. available at: probability.ca\/MT.","DOI":"10.1007\/978-1-4471-3267-7"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/229542.229547"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-8853-9"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192394"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863568"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.05.021"},{"key":"e_1_2_2_43_1","volume-title":"Proving Expected Sensitivity of Probabilistic Programs with Randomized Variable-Dependent Termination Time. CoRR abs\/1902.04744","author":"Wang Peixin","year":"2019","unstructured":"Peixin Wang , Hongfei Fu , Krishnendu Chatterjee , Yuxin Deng , and Ming Xu. 2019a. Proving Expected Sensitivity of Probabilistic Programs with Randomized Variable-Dependent Termination Time. CoRR abs\/1902.04744 ( 2019 ). arXiv: 1902.04744 http:\/\/arxiv.org\/abs\/1902.04744 Peixin Wang, Hongfei Fu, Krishnendu Chatterjee, Yuxin Deng, and Ming Xu. 2019a. Proving Expected Sensitivity of Probabilistic Programs with Randomized Variable-Dependent Termination Time. CoRR abs\/1902.04744 (2019). arXiv: 1902.04744 http:\/\/arxiv.org\/abs\/1902.04744"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314581"},{"key":"e_1_2_2_45_1","volume-title":"Probability with Martingales","author":"Williams David","unstructured":"David Williams . 1991. Probability with Martingales . Cambridge University Press . David Williams. 1991. Probability with Martingales. Cambridge University Press."},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110254"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371093","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371093","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:05:43Z","timestamp":1750273543000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371093"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12,20]]},"references-count":46,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2020,1]]}},"alternative-id":["10.1145\/3371093"],"URL":"https:\/\/doi.org\/10.1145\/3371093","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,12,20]]},"assertion":[{"value":"2019-12-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}