{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T07:53:19Z","timestamp":1790927599372,"version":"4.1.0"},"reference-count":39,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2022,4,29]],"date-time":"2022-04-29T00:00:00Z","timestamp":1651190400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,4,29]]},"abstract":"<jats:p>We present a novel strongest-postcondition-style calculus for quantitative reasoning about non-deterministic programs with loops. Whereas existing quantitative weakest pre allows reasoning about the value of a quantity after a program terminates on a given initial state, quantitative strongest post allows reasoning about the value that a quantity had before the program was executed and reached a given final state. We show how strongest post enables reasoning about the flow of quantitative information through programs. Similarly to weakest liberal preconditions, we also develop a quantitative strongest liberal post. As a byproduct, we obtain the entirely unexplored notion of strongest liberal postconditions and show how these foreshadow a potential new program logic - partial incorrectness logic - which would be a more liberal version of O'Hearn's recent incorrectness logic.<\/jats:p>","DOI":"10.1145\/3527331","type":"journal-article","created":{"date-parts":[[2022,4,29]],"date-time":"2022-04-29T15:42:03Z","timestamp":1651246923000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":15,"title":["Quantitative strongest post: a calculus for reasoning about the flow of quantitative information"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1485-327X","authenticated-orcid":false,"given":"Linpeng","family":"Zhang","sequence":"first","affiliation":[{"name":"University College London, UK"}],"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":"Saarland University, Germany \/ University College London, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,4,29]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2020.09.002"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27864-1_10"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00291051"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434320"},{"key":"e_1_2_1_5_1","volume-title":"Joost-Pieter Katoen, Christoph Matheja, and Thomas Noll.","author":"Batz Kevin","year":"2018","unstructured":"Kevin Batz , Benjamin Lucien Kaminski , Joost-Pieter Katoen, Christoph Matheja, and Thomas Noll. 2018 . Quantitative Separation Logic. CoRR , abs\/1802.10467 (2018), https:\/\/doi.org\/10.48550\/arXiv.1802.10467 arxiv:1802.10467. Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Thomas Noll. 2018. Quantitative Separation Logic. CoRR, abs\/1802.10467 (2018), https:\/\/doi.org\/10.48550\/arXiv.1802.10467 arxiv:1802.10467."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470608"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1137\/0207005"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-32304-2_19"},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of the Second International Symposium on Programming. Dunod","author":"Cousot P.","unstructured":"P. Cousot and R. Cousot . 1976. Static determination of dynamic properties of programs . In Proceedings of the Second International Symposium on Programming. Dunod , Paris, France, 106\u2013130. P. Cousot and R. Cousot. 1976. Static determination of dynamic properties of programs. In Proceedings of the Second International Symposium on Programming. Dunod, Paris, France, 106\u2013130."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35873-9_10"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24690-6_12"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-3228-5"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_13"},{"key":"e_1_2_1_16_1","volume-title":"Flow Analysis of Computer Programs","author":"Hecht Matthew S.","unstructured":"Matthew S. Hecht . 1977. Flow Analysis of Computer Programs . Elsevier . Matthew S. Hecht. 1977. Flow Analysis of Computer Programs. Elsevier."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00290146"},{"key":"e_1_2_1_19_1","unstructured":"Claire Jones. 1990. Probabilistic Non-Determinism. Ph.D. Dissertation. University of Edinburgh UK.  Claire Jones. 1990. Probabilistic Non-Determinism. Ph.D. Dissertation. University of Edinburgh UK."},{"key":"e_1_2_1_21_1","volume-title":"A weakest pre-expectation semantics for mixed-sign expectations","author":"Kaminski Benjamin Lucien","unstructured":"Benjamin Lucien Kaminski and Joost-Pieter Katoen . 2017. A weakest pre-expectation semantics for mixed-sign expectations . In LICS. IEEE Computer Society , 1\u201312. https:\/\/doi.org\/10.48550\/arXiv.1703.07682 Benjamin Lucien Kaminski and Joost-Pieter Katoen. 2017. A weakest pre-expectation semantics for mixed-sign expectations. In LICS. IEEE Computer Society, 1\u201312. https:\/\/doi.org\/10.48550\/arXiv.1703.07682"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.2307\/2325085"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(85)90012-1"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/b138392"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/b138392"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-28644-8_4"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371078"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796897002906"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_14"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.2307\/1990888"},{"key":"e_1_2_1_32_1","volume-title":"Introduction to Static Analysis \u2013 An Abstract Interpretation Perspective","author":"Rival Xavier","unstructured":"Xavier Rival and Kwangkeun Yi. 2020. Introduction to Static Analysis \u2013 An Abstract Interpretation Perspective . MIT Press . Xavier Rival and Kwangkeun Yi. 2020. Introduction to Static Analysis \u2013 An Abstract Interpretation Perspective. MIT Press."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00596-1_21"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.2307\/2268810"},{"key":"e_1_2_1_35_1","volume-title":"Report of a Conference on High Speed Automatic Calculating Machines. Univ. Math. Lab.","author":"Turing Alan Mathison","unstructured":"Alan Mathison Turing . 1949. Checking a Large Routine . In Report of a Conference on High Speed Automatic Calculating Machines. Univ. Math. Lab. , Cambridge , 67\u201369. https:\/\/doi.org\/10.5555\/94938.94952 Alan Mathison Turing. 1949. Checking a Large Routine. In Report of a Conference on High Speed Automatic Calculating Machines. Univ. Math. Lab., Cambridge, 67\u201369. https:\/\/doi.org\/10.5555\/94938.94952"},{"key":"e_1_2_1_36_1","volume-title":"Perfectly Parallel Fairness Certification of Neural Networks. CoRR, abs\/1912.02499","author":"Urban Caterina","year":"2019","unstructured":"Caterina Urban , Maria Christakis , Valentin W\u00fcstholz , and Fuyuan Zhang . 2019. Perfectly Parallel Fairness Certification of Neural Networks. CoRR, abs\/1912.02499 ( 2019 ), https:\/\/doi.org\/10.48550\/arXiv.1912.02499 arxiv:1912.02499. Caterina Urban, Maria Christakis, Valentin W\u00fcstholz, and Fuyuan Zhang. 2019. Perfectly Parallel Fairness Certification of Neural Networks. CoRR, abs\/1912.02499 (2019), https:\/\/doi.org\/10.48550\/arXiv.1912.02499 arxiv:1912.02499."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_24"},{"key":"e_1_2_1_38_1","volume-title":"Proceedings of the 7th International Joint Conference CAAP\/FASE on Theory and Practice of Software Development (TAPSOFT \u201997)","author":"Dennis","unstructured":"Dennis M. Volpano and Geoffrey Smith. 1997. A Type-Based Approach to Program Security . In Proceedings of the 7th International Joint Conference CAAP\/FASE on Theory and Practice of Software Development (TAPSOFT \u201997) . Springer-Verlag, Berlin, Heidelberg. 607\u2013621. isbn:3540627812 https:\/\/doi.org\/10945\/35283 Dennis M. Volpano and Geoffrey Smith. 1997. A Type-Based Approach to Program Security. In Proceedings of the 7th International Joint Conference CAAP\/FASE on Theory and Practice of Software Development (TAPSOFT \u201997). Springer-Verlag, Berlin, Heidelberg. 607\u2013621. isbn:3540627812 https:\/\/doi.org\/10945\/35283"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.330.11"},{"key":"e_1_2_1_40_1","volume-title":"Quantitative Strongest Post. CoRR, abs\/2202.06765","author":"Zhang Linpeng","year":"2022","unstructured":"Linpeng Zhang and Benjamin Lucien Kaminski . 2022. Quantitative Strongest Post. CoRR, abs\/2202.06765 ( 2022 ), https:\/\/doi.org\/10.48550\/ARXIV.2202.06765 arXiv:2202.06765. Linpeng Zhang and Benjamin Lucien Kaminski. 2022. Quantitative Strongest Post. CoRR, abs\/2202.06765 (2022), https:\/\/doi.org\/10.48550\/ARXIV.2202.06765 arXiv:2202.06765."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3527331","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3527331","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:18:53Z","timestamp":1750191533000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3527331"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,4,29]]},"references-count":39,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2022,4,29]]}},"alternative-id":["10.1145\/3527331"],"URL":"https:\/\/doi.org\/10.1145\/3527331","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,4,29]]},"assertion":[{"value":"2022-04-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}