{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T07:53:15Z","timestamp":1790927595866,"version":"4.1.0"},"reference-count":46,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T00:00:00Z","timestamp":1546387200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["401\/2-1"],"award-info":[{"award-number":["401\/2-1"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"name":"DFG","award":["RTG 2236 UnRAVeL"],"award-info":[{"award-number":["RTG 2236 UnRAVeL"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,1,2]]},"abstract":"<jats:p>\n            We present\n            <jats:italic>quantitative separation logic<\/jats:italic>\n            (QSL). In contrast to classical separation logic, QSL employs quantities which evaluate to real numbers instead of predicates which evaluate to Boolean values. The connectives of classical separation logic, separating conjunction and separating implication, are lifted from predicates to quantities. This extension is conservative: Both connectives are backward compatible to their classical analogs and obey the same laws, e.g. modus ponens, adjointness, etc.\n          <\/jats:p>\n          <jats:p>\n            Furthermore, we develop a weakest precondition calculus for quantitative reasoning about\n            <jats:italic>probabilistic pointer programs<\/jats:italic>\n            in QSL. This calculus is a conservative extension of both Ishtiaq\u2019s, O\u2019Hearn\u2019s and Reynolds\u2019 separation logic for heap-manipulating programs and Kozen\u2019s \/ McIver and Morgan\u2019s weakest preexpectations for probabilistic programs. Soundness is proven with respect to an operational semantics based on Markov decision processes. Our calculus preserves O\u2019Hearn\u2019s\n            <jats:italic>frame rule<\/jats:italic>\n            , which enables local reasoning. We demonstrate that our calculus enables reasoning about quantities such as the probability of terminating with an empty heap, the probability of reaching a certain array permutation, or the expected length of a list.\n          <\/jats:p>","DOI":"10.1145\/3290347","type":"journal-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:51Z","timestamp":1546608831000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":37,"title":["Quantitative separation logic: a logic for reasoning about probabilistic pointer programs"],"prefix":"10.1145","volume":"3","author":[{"given":"Kevin","family":"Batz","sequence":"first","affiliation":[{"name":"RWTH Aachen University, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Benjamin Lucien","family":"Kaminski","sequence":"additional","affiliation":[{"name":"RWTH Aachen University, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[{"name":"RWTH Aachen University, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Christoph","family":"Matheja","sequence":"additional","affiliation":[{"name":"RWTH Aachen University, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thomas","family":"Noll","sequence":"additional","affiliation":[{"name":"RWTH Aachen University, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,1,2]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(01)00230-7"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/6490.6494"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1989.63531"},{"key":"e_1_2_2_4_1","volume-title":"Amortised Resource Analysis with Separation Logic. Logical Methods in Computer Science 7, 2","author":"Atkey Robert","year":"2011"},{"key":"e_1_2_2_5_1","volume-title":"Principles of Model Checking","author":"Baier Christel"},{"key":"e_1_2_2_6_1","volume-title":"An AssertionBased Program Logic for Probabilistic Programs. In ESOP","author":"Barthe Gilles","year":"2018"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31113-0_1"},{"key":"e_1_2_2_8_1","volume-title":"Joost-Pieter Katoen, Christoph Matheja, and Thomas Noll.","author":"Batz Kevin","year":"2018"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/277651.277660"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9179-9"},{"key":"e_1_2_2_11_1","doi-asserted-by":"crossref","unstructured":"James Brotherston. 2007. Formalised Inductive Reasoning in the Logic of Bunched Implications. In SAS. 87\u2013103.   James Brotherston. 2007. Formalised Inductive Reasoning in the Logic of Bunched Implications. In SAS. 87\u2013103.","DOI":"10.1007\/978-3-540-74061-2_6"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2958738"},{"key":"e_1_2_2_13_1","volume-title":"CAV (LNCS)","author":"Chakarov Aleksandar"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328469"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837639"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2010.07.004"},{"key":"e_1_2_2_17_1","volume-title":"Introduction to Algorithms","author":"Cormen Thomas H.","edition":"3"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1979.82.43"},{"key":"e_1_2_2_19_1","unstructured":"Edsger Wybe Dijkstra. 1976. A Discipline of Programming. Prentice\u2013Hall.  Edsger Wybe Dijkstra. 1976. A Discipline of Programming. Prentice\u2013Hall."},{"key":"e_1_2_2_20_1","volume-title":"Probabilistic Machines Can Use Less Running Time. In IFIP Congress","volume":"839","author":"Freivalds Rusins","year":"1977"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.peva.2013.11.004"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00450-013-0251-7"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211249"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/5.1.10"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.375719"},{"key":"e_1_2_2_27_1","unstructured":"Claire Jones. 1990. Probabilistic Non\u2013Determinism. Ph.D. Dissertation. University of Edinburgh UK.  Claire Jones. 1990. Probabilistic Non\u2013Determinism. Ph.D. Dissertation. University of Edinburgh UK."},{"key":"e_1_2_2_28_1","volume-title":"ESOP (LNCS)","author":"Kaminski Benjamin Lucien"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.2307\/2325085"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1979.38"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/800061.808758"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_2_2_33_1","first-page":"5","article-title":"Inferring invariants in separation logic for imperative list-processing programs","volume":"1","author":"Magill Stephen","year":"2006","journal-title":"SPACE"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/274787.274812"},{"key":"e_1_2_2_35_1","volume-title":"Refinement and Proof for Probabilistic Systems","author":"McIver Annabelle"},{"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":"publisher","DOI":"10.1145\/229542.229547"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192394"},{"key":"e_1_2_2_39_1","unstructured":"Peter W. O\u2019Hearn. 2012. A Primer on Separation Logic (and Automatic Program Verification and Analysis). In Software Safety and Security - Tools for Analysis and Verification. 286\u2013318.  Peter W. O\u2019Hearn. 2012. A Primer on Separation Logic (and Automatic Program Verification and Analysis). In Software Safety and Security - Tools for Analysis and Verification. 286\u2013318."},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2935317"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/78973.78977"},{"key":"e_1_2_2_42_1","volume-title":"Markov Decision Processes: Discrete Stochastic Dynamic Programming","author":"Puterman Martin Lee"},{"key":"e_1_2_2_43_1","volume-title":"Separation Logic: A Logic for Shared Mutable Data Structures","author":"Reynolds John Charles","year":"2002"},{"key":"e_1_2_2_44_1","volume-title":"The Algebraic Intepretation of Quantifiers. Intuitionistic and Classical. Andrzej Mostowski and Foundational Studies","author":"Scott Dana","year":"2008"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290377"},{"key":"e_1_2_2_46_1","volume-title":"O\u2019Hearn","author":"Yang Hongseok","year":"2002"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290347","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290347","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:58:04Z","timestamp":1750208284000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290347"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":46,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290347"],"URL":"https:\/\/doi.org\/10.1145\/3290347","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,2]]},"assertion":[{"value":"2019-01-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}