{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T07:59:06Z","timestamp":1770278346066,"version":"3.49.0"},"reference-count":34,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"ERC Advanced Research Grant FRAPPANT","award":["787914"],"award-info":[{"award-number":["787914"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,1,7]]},"abstract":"<jats:p>We study Hoare-like logics, including partial and total correctness Hoare logic, incorrectness logic, Lisbon logic, and many others through the lens of predicate transformers \u00e0 la Dijkstra and through the lens of Kleene algebra with top and tests (TopKAT). Our main goal is to give an overview \u2013 a taxonomy \u2013 of how these program logics relate, in particular under different assumptions like for example program termination, determinism, and reversibility. As a byproduct, we obtain a TopKAT characterization of Lisbon logic, which \u2013 to the best of our knowledge \u2013 is a novel result.<\/jats:p>","DOI":"10.1145\/3704896","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"1782-1811","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["A Taxonomy of Hoare-Like Logics: Towards a Holistic View using Predicate Transformers and Kleene Algebras with Top and Tests"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6823-7918","authenticated-orcid":false,"given":"Lena","family":"Verscht","sequence":"first","affiliation":[{"name":"Saarland University, Saarbr\u00fccken, Germany"},{"name":"RWTH Aachen University, Aachen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5185-2324","authenticated-orcid":false,"given":"Benjamin Lucien","family":"Kaminski","sequence":"additional","affiliation":[{"name":"Saarland University, Saarbr\u00fccken, Germany"},{"name":"University College London, London, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_1","unstructured":"Flavio Ascari Roberto Bruni Roberta Gori and Francesco Logozzo. 2024. Sufficient Incorrectness Logic: SIL and Separation SIL. arXiv:2310.18156 [cs.LO] https:\/\/arxiv.org\/abs\/2310.18156"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3582267"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/10722010_4"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632849"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35873-9_10"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24690-6_12"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005251"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_3_2_11_1","volume-title":"A discipline of programming","author":"Dijkstra Edsger W.","year":"1976","unstructured":"Edsger W. Dijkstra. 1976. A discipline of programming. Vol. 613924118. Prentice Hall PTR."},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-3228-5"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/540175"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/322077.322088"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.2168\/lmcs-7(1:1)2011"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3208102"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/256167.256195"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2023.19"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/b138392"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-22308-2_16"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-88701-8_20"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/11734673_16"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/229542.229547"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371078"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3689720"},{"key":"e_1_3_2_27_1","volume-title":"Introduction to Static Analysis \u2013 An Abstract Interpretation Perspective","author":"Rival Xavier","year":"2020","unstructured":"Xavier Rival and Kwangkeun Yi. 2020. Introduction to Static Analysis \u2013 An Abstract Interpretation Perspective. MIT Press."},{"key":"e_1_3_2_28_1","unstructured":"Lena Verscht and Benjamin Kaminski. 2023. Hoare-Like Triples and Kleene Algebras with Top and Tests: Towards a Holistic Perspective on Hoare Logic Incorrectness Logic and Beyond. arXiv:2312.09662 [cs.LO] https:\/\/arxiv.org\/abs\/2312.09662"},{"key":"e_1_3_2_29_1","doi-asserted-by":"crossref","unstructured":"Lena Verscht and Benjamin Lucien Kaminski. 2024. A Taxonomy of Hoare-Like Logics: Towards a Holistic View using Predicate Transformers and Kleene Algebras with Top and Tests. arXiv:2411.06416 [cs.PL] https:\/\/arxiv.org\/abs\/2411.06416","DOI":"10.1145\/3704896"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45442-X_14"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2003.09.002"},{"key":"e_1_3_2_32_1","unstructured":"John Wickerson. 2024. What is the Other Incorrectness Logic? https:\/\/johnwickerson.wordpress.com\/2024\/02\/15\/what-is-the-other-incorrectness-logic\/."},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498690"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2202.06765"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586045"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704896","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704896","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:16:04Z","timestamp":1770200164000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704896"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":34,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704896"],"URL":"https:\/\/doi.org\/10.1145\/3704896","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-11","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}