{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:06:28Z","timestamp":1767927988752,"version":"3.49.0"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031911170","type":"print"},{"value":"9783031911187","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Concurrent randomized programs in the oblivious adversary model are extremely difficult for modular verification because\u00a0the interaction between threads is very sensitive to\u00a0the program structure and the execution steps. We propose a new program logic supporting thread-local verification. With a novel \u201csplit\u201d mechanism,\u00a0one can split the state distribution into smaller partitions, and the reasoning can be done based on each partition independently, which allows us\u00a0to avoid considering different execution paths of branch statements simultaneously. The logic rules are compositional and are natural extensions of their sequential counterparts. Using our program logic, we verify four typical algorithms in the oblivious adversary model.<\/jats:p>","DOI":"10.1007\/978-3-031-91118-7_13","type":"book-chapter","created":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T08:17:28Z","timestamp":1746001048000},"page":"322-348","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["A Program Logic for Concurrent Randomized Programs in the Oblivious Adversary Model"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-0853-0168","authenticated-orcid":false,"given":"Weijie","family":"Fan","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4337-6548","authenticated-orcid":false,"given":"Hongjin","family":"Liang","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3972-9395","authenticated-orcid":false,"given":"Xinyu","family":"Feng","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5965-1209","authenticated-orcid":false,"given":"Hanru","family":"Jiang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"13_CR1","doi-asserted-by":"publisher","unstructured":"Aguirre, A., Barthe, G., Hsu, J., Kaminski, B.L., Katoen, J.P., Matheja, C.: A pre-expectation calculus for probabilistic sensitivity. Proc. ACM Program. Lang. 5(POPL) (jan 2021). https:\/\/doi.org\/10.1145\/3434333, https:\/\/doi.org\/10.1145\/3434333","DOI":"10.1145\/3434333"},{"key":"13_CR2","doi-asserted-by":"publisher","unstructured":"Alistarh, D., Aspnes, J.: Sub-logarithmic test-and-set against a weak adversary. In: Proceedings of the 25th International Conference on Distributed Computing. pp. 97\u2013109. DISC\u201911, Springer-Verlag, Berlin, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24100-0_7","DOI":"10.1007\/978-3-642-24100-0_7"},{"key":"13_CR3","doi-asserted-by":"publisher","unstructured":"Aspnes, J.: Randomized protocols for asynchronous consensus. Distributed Comput. 16(2-3), 165\u2013175 (2003). https:\/\/doi.org\/10.1007\/s00446-002-0081-5, https:\/\/doi.org\/10.1007\/s00446-002-0081-5","DOI":"10.1007\/s00446-002-0081-5"},{"key":"13_CR4","unstructured":"Aspnes, J.: Notes on randomized algorithms (2023), https:\/\/www.cs.yale.edu\/homes\/aspnes\/classes\/469\/notes.pdf"},{"key":"13_CR5","unstructured":"Aspnes, J.: Notes on theory of distributed systems (2023), https:\/\/www.cs.yale.edu\/homes\/aspnes\/classes\/465\/notes.pdf"},{"key":"13_CR6","doi-asserted-by":"publisher","unstructured":"Barthe, G., Espitau, T., Gaboardi, M., Gr\u00e9goire, B., Hsu, J., Strub, P.: An assertion-based program logic for probabilistic programs. In: Proceedings of the 27th European Symposium on Programming (ESOP 2018). pp. 117\u2013144. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-89884-1_5, https:\/\/doi.org\/10.1007\/978-3-319-89884-1_5","DOI":"10.1007\/978-3-319-89884-1_5"},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"Barthe, G., Hsu, J., Liao, K.: A probabilistic separation logic. Proc. ACM Program. Lang. 4(POPL), 55:1\u201355:30 (2020)","DOI":"10.1145\/3371123"},{"key":"13_CR8","doi-asserted-by":"publisher","unstructured":"Batz, K., Kaminski, B.L., Katoen, J.P., Matheja, C.: Relatively complete verification of probabilistic programs: An expressive language for expectation-based reasoning. Proc. ACM Program. Lang. 5(POPL) (jan 2021). https:\/\/doi.org\/10.1145\/3434320, https:\/\/doi.org\/10.1145\/3434320","DOI":"10.1145\/3434320"},{"key":"13_CR9","doi-asserted-by":"publisher","unstructured":"Batz, K., Kaminski, B.L., Katoen, J.P., Matheja, C., Noll, T.: Quantitative separation logic: A logic for reasoning about probabilistic pointer programs. Proc. ACM Program. Lang. 3(POPL) (jan 2019). https:\/\/doi.org\/10.1145\/3290347, https:\/\/doi.org\/10.1145\/3290347","DOI":"10.1145\/3290347"},{"key":"13_CR10","doi-asserted-by":"publisher","unstructured":"Bertrand, N., Konnov, I., Lazic, M., Widder, J.: Verification of randomized consensus algorithms under round-rigid adversaries. In: Fokkink, W.J., van Glabbeek, R. (eds.) Proceedings of the 30th International Conference on Concurrency Theory (CONCUR 2019). LIPIcs, vol.\u00a0140, pp. 33:1\u201333:15. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2019). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2019.33, https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2019.33","DOI":"10.4230\/LIPIcs.CONCUR.2019.33"},{"key":"13_CR11","doi-asserted-by":"publisher","unstructured":"Bertrand, N., Lazic, M., Widder, J.: A reduction theorem for randomized distributed algorithms under weak adversaries. In: Henglein, F., Shoham, S., Vizel, Y. (eds.) Proceedings of the 22nd International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2021). Lecture Notes in Computer Science, vol. 12597, pp. 219\u2013239. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-67067-2_11, https:\/\/doi.org\/10.1007\/978-3-030-67067-2_11","DOI":"10.1007\/978-3-030-67067-2_11"},{"key":"13_CR12","doi-asserted-by":"publisher","unstructured":"Chor, B., Israeli, A., Li, M.: Wait-free consensus using asynchronous hardware. SIAM Journal on Computing 23(4), 701\u2013712 (1994). https:\/\/doi.org\/10.1137\/S0097539790192635, https:\/\/doi.org\/10.1137\/S0097539790192635","DOI":"10.1137\/S0097539790192635"},{"key":"13_CR13","unstructured":"Fan, W., Liang, H., Feng, X., Jiang, H.: A program logic for concurrent randomized programs in the oblivious adversary model. Tech. rep. (2025), https:\/\/plax-lab.github.io\/publications\/randoa\/randoa-tr.pdf"},{"key":"13_CR14","doi-asserted-by":"publisher","unstructured":"Fesefeldt, I., Katoen, J., Noll, T.: Towards concurrent quantitative separation logic. In: Proceedings of 33rd International Conference on Concurrency Theory (CONCUR 2022). pp. 25:1\u201325:24 (2022). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2022.25, https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2022.25","DOI":"10.4230\/LIPIcs.CONCUR.2022.25"},{"key":"13_CR15","doi-asserted-by":"publisher","unstructured":"Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst. 5(4), 596\u2013619 (oct 1983). https:\/\/doi.org\/10.1145\/69575.69577, https:\/\/doi.org\/10.1145\/69575.69577","DOI":"10.1145\/69575.69577"},{"key":"13_CR16","doi-asserted-by":"publisher","unstructured":"Jung, R., Swasey, D., Sieczkowski, F., Svendsen, K., Turon, A., Birkedal, L., Dreyer, D.: Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. In: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. p. 637-650. POPL \u201915, Association for Computing Machinery, New York, NY, USA (2015). https:\/\/doi.org\/10.1145\/2676726.2676980, https:\/\/doi.org\/10.1145\/2676726.2676980","DOI":"10.1145\/2676726.2676980"},{"key":"13_CR17","doi-asserted-by":"publisher","unstructured":"McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science, Springer (2005). https:\/\/doi.org\/10.1007\/b138392, https:\/\/doi.org\/10.1007\/b138392","DOI":"10.1007\/b138392"},{"key":"13_CR18","doi-asserted-by":"publisher","unstructured":"McIver, A., Rabehaja, T.M., Struth, G.: Probabilistic rely-guarantee calculus. Theor. Comput. Sci. 655, 120\u2013134 (2016). https:\/\/doi.org\/10.1016\/j.tcs.2016.01.016, https:\/\/doi.org\/10.1016\/j.tcs.2016.01.016","DOI":"10.1016\/j.tcs.2016.01.016"},{"key":"13_CR19","doi-asserted-by":"publisher","unstructured":"Rand, R., Zdancewic, S.: VPHL: A verified partial-correctness logic for probabilistic programs. In: Ghica, D.R. (ed.) Proceedings of the 31st Conference on the Mathematical Foundations of Programming Semantics (MFPS 2015). Electronic Notes in Theoretical Computer Science, vol.\u00a0319, pp. 351\u2013367. Elsevier (2015). https:\/\/doi.org\/10.1016\/j.entcs.2015.12.021, https:\/\/doi.org\/10.1016\/j.entcs.2015.12.021","DOI":"10.1016\/j.entcs.2015.12.021"},{"key":"13_CR20","doi-asserted-by":"publisher","unstructured":"Tassarotti, J., Harper, R.: A separation logic for concurrent randomized programs. Proc. ACM Program. Lang. 3(POPL) (jan 2019). https:\/\/doi.org\/10.1145\/3290377, https:\/\/doi.org\/10.1145\/3290377","DOI":"10.1145\/3290377"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-91118-7_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T08:17:33Z","timestamp":1746001053000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-91118-7_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031911170","9783031911187"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-91118-7_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/esop\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}