{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T20:16:16Z","timestamp":1784837776194,"version":"3.55.0"},"reference-count":56,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T00:00:00Z","timestamp":1609718400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["787914"],"award-info":[{"award-number":["787914"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2021,1,4]]},"abstract":"<jats:p>\n                    We study\n                    <jats:italic toggle=\"yes\">a syntax for specifying quantitative<\/jats:italic>\n                    <jats:italic toggle=\"yes\">assertions<\/jats:italic>\n                    \u2014functions mapping program states to numbers\u2014for probabilistic program verification. We prove that our syntax is expressive in the following sense: Given any probabilistic program\n                    <jats:italic toggle=\"yes\">C<\/jats:italic>\n                    , if a function\n                    <jats:italic toggle=\"yes\">f<\/jats:italic>\n                    is expressible in our syntax, then the function mapping each initial state \u03c3 to the expected value of evaluated in the final states reached after termination of\n                    <jats:italic toggle=\"yes\">C<\/jats:italic>\n                    on \u03c3 (also called the weakest preexpectation wp[\n                    <jats:italic toggle=\"yes\">C<\/jats:italic>\n                    ](\n                    <jats:italic toggle=\"yes\">f<\/jats:italic>\n                    )) is also expressible in our syntax.\n                  <\/jats:p>\n                  <jats:p>\n                    As a consequence, we obtain a\n                    <jats:italic toggle=\"yes\">relatively complete verification system<\/jats:italic>\n                    for reasoning about expected values and probabilities in the sense of Cook: Apart from proving a single inequality between two functions given by syntactic expressions in our language, given\n                    <jats:italic toggle=\"yes\">f<\/jats:italic>\n                    ,\n                    <jats:italic toggle=\"yes\">g<\/jats:italic>\n                    , and\n                    <jats:italic toggle=\"yes\">C<\/jats:italic>\n                    , we can check whether\n                    <jats:italic toggle=\"yes\">g<\/jats:italic>\n                    \u227c wp[\n                    <jats:italic toggle=\"yes\">C<\/jats:italic>\n                    ](\n                    <jats:italic toggle=\"yes\">f<\/jats:italic>\n                    ).\n                  <\/jats:p>","DOI":"10.1145\/3434320","type":"journal-article","created":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T12:34:24Z","timestamp":1609763664000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":33,"title":["Relatively complete verification of probabilistic programs: an expressive language for expectation-based reasoning"],"prefix":"10.1145","volume":"5","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8705-2564","authenticated-orcid":false,"given":"Kevin","family":"Batz","sequence":"first","affiliation":[{"name":"RWTH Aachen University, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5185-2324","authenticated-orcid":false,"given":"Benjamin Lucien","family":"Kaminski","sequence":"additional","affiliation":[{"name":"University College London, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6143-1926","authenticated-orcid":false,"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[{"name":"RWTH Aachen University, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9151-0441","authenticated-orcid":false,"given":"Christoph","family":"Matheja","sequence":"additional","affiliation":[{"name":"ETH Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,1,4]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-019-00501-3"},{"key":"e_1_2_1_2_1","volume-title":"Joost-Pieter Katoen, and Christoph Matheja.","author":"Batz Kevin","year":"2020","unstructured":"Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. 2020. Relatively Complete Verification of Probabilistic Programs-Extended Version. CoRR ( 2020 ). to appear."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290347"},{"key":"e_1_2_1_4_1","unstructured":"Joseph Bertrand. 1849. Trait\u00e9 d'Arithm\u00e9tique. Libraire de L. Hachette et Cie."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32033-3_24"},{"key":"e_1_2_1_6_1","article-title":"Ein Beitrag zur Mannigfaltigkeitslehre","volume":"1878","author":"Cantor Georg","year":"1878","unstructured":"Georg Cantor. 1878. Ein Beitrag zur Mannigfaltigkeitslehre. Journal f\u00fcr die reine und angewandte Mathematik 1878, 84 ( 1878 ), 242-258.","journal-title":"Journal f\u00fcr die reine und angewandte Mathematik"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_1"},{"key":"e_1_2_1_9_1","first-page":"327","volume-title":"Proceedings of the 43rd Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, POPL 2016, St","author":"Chatterjee Krishnendu","year":"2016","unstructured":"Krishnendu Chatterjee, Hongfei Fu, Petr Novotn\u00fd, and Rouzbeh Hasheminezhad. 2016b. Algorithmic analysis of qualitative and quantitative termination problems for afine probabilistic programs. In Proceedings of the 43rd Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20-22, 2016, Rastislav Bod\u00edk and Rupak Majumdar (Eds.). ACM, 327-342."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3174800"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009873"},{"key":"e_1_2_1_12_1","series-title":"SIAM J. Comput. 7 ( 1978 ), 70-90","volume-title":"Soundness and Completeness of an Axiom System for Program Verification","author":"Cook Stephen A.","unstructured":"Stephen A. Cook. 1978. Soundness and Completeness of an Axiom System for Program Verification. SIAM J. Comput. 7 ( 1978 ), 70-90."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_9"},{"key":"e_1_2_1_14_1","article-title":"Verifying Probabilistic Programs Using a Hoare Like","volume":"13","author":"den Hartog Jerry","year":"2002","unstructured":"Jerry den Hartog and Erik P. de Vink. 2002. Verifying Probabilistic Programs Using a Hoare Like Logic. Int. J. Found. Comput. Sci. 13, 3 ( 2002 ), 315-340.","journal-title":"Logic. Int. J. Found. Comput. Sci."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-27810-0_6"},{"key":"e_1_2_1_16_1","volume-title":"A Discipline of Programming","author":"Dijkstra Edsger W.","year":"1958","unstructured":"Edsger W. Dijkstra. 1976. A Discipline of Programming. Prentice-Hall. http:\/\/www.worldcat.org\/oclc\/01958445"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-68167-2_26"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677001"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1137\/1.9781611973082.15"},{"key":"e_1_2_1_20_1","first-page":"19","volume-title":"Schwarz (Ed.)","volume":"19","author":"Floyd Robert W","year":"1967","unstructured":"Robert W Floyd. 1967. Assigning Meanings to Programs. In Mathematical Aspects of Computer Science, J.T. Schwarz (Ed.), Vol. 19. American Mathematical Society, 19-32."},{"key":"e_1_2_1_21_1","first-page":"468","volume-title":"VMCAI 2019, Cascais, Portugal, January 13-15, 2019, Proceedings (Lecture Notes in Computer Science","volume":"11388","author":"Fu Hongfei","year":"2019","unstructured":"Hongfei Fu and Krishnendu Chatterjee. 2019. Termination of Nondeterministic Probabilistic Programs. In Verification, Model Checking, and Abstract Interpretation-20th International Conference, VMCAI 2019, Cascais, Portugal, January 13-15, 2019, Proceedings (Lecture Notes in Computer Science, Vol. 11388 ), Constantin Enea and Ruzica Piskac (Eds.). Springer, 468-490."},{"key":"e_1_2_1_22_1","doi-asserted-by":"crossref","unstructured":"Kurt G\u00f6del. 1931. \u00dcber formal unentscheidbare S\u00e4tze der Principia Mathematica und verwandter Systeme I. Monatshefte f\u00fcr Mathematik und Physik 38 1 ( 1931 ) 173-198.","DOI":"10.1007\/BF01700692"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.peva"},{"key":"e_1_2_1_24_1","first-page":"1","volume-title":"Termination of Probabilistic Concurrent Programs. In Conference Record of the Ninth Annual ACM Symposium on Principles of Programming Languages","author":"Hart Sergiu","year":"1982","unstructured":"Sergiu Hart, Micha Sharir, and Amir Pnueli. 1982. Termination of Probabilistic Concurrent Programs. In Conference Record of the Ninth Annual ACM Symposium on Principles of Programming Languages, Albuquerque, New Mexico, USA, January 1982, Richard A. DeMillo (Ed.). ACM Press, 1-6."},{"key":"e_1_2_1_25_1","doi-asserted-by":"crossref","unstructured":"C. A. R. Hoare. 1969. An Axiomatic Basis for Computer Programming. Commun. ACM 12 10 ( 1969 ) 576-580.","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-02768-1_11"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360555"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1460833.1460872"},{"key":"e_1_2_1_29_1","unstructured":"Benjamin Lucien Kaminski. 2019. Advanced weakest precondition calculi for probabilistic programs. Ph.D. Dissertation. RWTH Aachen University Germany. http:\/\/publications.rwth-aachen.de\/record\/755408"},{"key":"e_1_2_1_30_1","first-page":"307","volume-title":"MFCS 2015, Milan, Italy, August 24-28, 2015, Proceedings, Part I (Lecture Notes in Computer Science","volume":"9234","author":"Kaminski Benjamin Lucien","year":"2015","unstructured":"Benjamin Lucien Kaminski and Joost-Pieter Katoen. 2015. On the Hardness of Almost-Sure Termination. In Mathematical Foundations of Computer Science 2015-40th International Symposium, MFCS 2015, Milan, Italy, August 24-28, 2015, Proceedings, Part I (Lecture Notes in Computer Science, Vol. 9234 ), Giuseppe F. Italiano, Giovanni Pighizzini, and Donald Sannella (Eds.). Springer, 307-318."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005153"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-018-0321-1"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3208102"},{"key":"e_1_2_1_34_1","volume-title":"Morgan","author":"Katoen Joost-Pieter","year":"2010","unstructured":"Joost-Pieter Katoen, Annabelle McIver, Larissa Meinicke, and Carroll C. Morgan. 2010. Linear-Invariant Generation for Probabilistic Programs:-Automated Support for Proof-Based Methods. In SAS (Lecture Notes in Computer Science, Vol. 6337 ). Springer, 390-406."},{"key":"e_1_2_1_35_1","volume-title":"J de Groot, and Adriaan Cornelis Zaanen.","author":"Kleene Stephen Cole","year":"1952","unstructured":"Stephen Cole Kleene, NG De Bruijn, J de Groot, and Adriaan Cornelis Zaanen. 1952. Introduction to Metamathematics. Vol. 483. van Nostrand New York."},{"key":"e_1_2_1_36_1","first-page":"101","volume-title":"Semantics of Probabilistic Programs. In 20th Annual Symposium on Foundations of Computer Science","author":"Kozen Dexter","year":"1979","unstructured":"Dexter Kozen. 1979. Semantics of Probabilistic Programs. In 20th Annual Symposium on Foundations of Computer Science, San Juan, Puerto Rico, 29-31 October 1979. IEEE Computer Society, 101-114."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(81)90036-2"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/800061.808758"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(85)90012-1"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/343369.343378"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0255(01)00164-5"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-322-96753-4"},{"key":"e_1_2_1_43_1","unstructured":"J. Loeckx K. Sieber and R.D. Stansifer. 1984. The Foundations of Program Verification. John Wiley. https:\/\/books.google.de\/ books?id=wagmAAAAMAAJ"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.18154\/RWTH-2020-00940"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/b138392"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158121"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1201\/9781420049503-c16"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192394"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3156018"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2935317"},{"key":"e_1_2_1_51_1","volume-title":"Separation Logic: A Logic for Shared Mutable Data Structures. In 17th IEEE Symposium on Logic in Computer Science (LICS 2002 )","author":"Reynolds John C.","year":"2002","unstructured":"John C. Reynolds. 2002. Separation Logic: A Logic for Shared Mutable Data Structures. In 17th IEEE Symposium on Logic in Computer Science (LICS 2002 ), 22-25 July 2002, Copenhagen, Denmark, Proceedings. IEEE Computer Society, 55-74."},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.2307\/2266510"},{"key":"e_1_2_1_53_1","volume-title":"Polynomial Probabilistic Invariants and the Optional Stopping Theorem. CoRR abs\/","author":"Schreuder Anne","year":"1910","unstructured":"Anne Schreuder and C.-H. Luke Ong. 2019. Polynomial Probabilistic Invariants and the Optional Stopping Theorem. CoRR abs\/ 1910.12634 ( 2019 )."},{"key":"e_1_2_1_54_1","first-page":"179","article-title":"Completeness of Pointer Program Verification by Separation Logic. In Software Engineering and Formal Methods","author":"Tatsuta Makoto","year":"2009","unstructured":"Makoto Tatsuta, Wei-Ngan Chin, and Mahmudul Faisal Al Ameen. 2009. Completeness of Pointer Program Verification by Separation Logic. In Software Engineering and Formal Methods. IEEE Computer Society, 179-188.","journal-title":"IEEE Computer Society"},{"key":"e_1_2_1_55_1","doi-asserted-by":"crossref","unstructured":"Makoto Tatsuta Wei-Ngan Chin and Mahmudul Faisal Al Ameen. 2019. Completeness and expressiveness of pointer program verification by separation logic. Inf. Comput. 267 ( 2019 ) 1-27.","DOI":"10.1016\/j.ic.2019.03.002"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.5555\/151145"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434320","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434320","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T07:25:49Z","timestamp":1781853949000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434320"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,4]]},"references-count":56,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2021,1,4]]}},"alternative-id":["10.1145\/3434320"],"URL":"https:\/\/doi.org\/10.1145\/3434320","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,1,4]]},"assertion":[{"value":"2021-01-04","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}