{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T10:50:27Z","timestamp":1770288627610,"version":"3.49.0"},"reference-count":31,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T00:00:00Z","timestamp":1641945600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS2040249,CNS2040222"],"award-info":[{"award-number":["CNS2040249,CNS2040222"]}],"id":[{"id":"10.13039\/100000001","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":[[2022,1,16]]},"abstract":"<jats:p>Kleene algebra with tests (KAT) is a foundational equational framework for reasoning about programs, which has found applications in program transformations, networking and compiler optimizations, among many other areas. In his seminal work, Kozen proved that KAT subsumes propositional Hoare logic, showing that one can reason about the (partial) correctness of while programs by means of the equational theory of KAT.<\/jats:p>\n          <jats:p>In this work, we investigate the support that KAT provides for reasoning about incorrectness, instead, as embodied by O'Hearn's recently proposed incorrectness logic. We show that KAT cannot directly express incorrectness logic. The main reason for this limitation can be traced to the fact that KAT cannot express explicitly the notion of codomain, which is essential to express incorrectness triples. To address this issue, we study Kleene Algebra with Top and Tests (TopKAT), an extension of KAT with a top element. We show that TopKAT is powerful enough to express a codomain operation, to express incorrectness triples, and to prove all the rules of incorrectness logic sound. This shows that one can reason about the incorrectness of while-like programs by means of the equational theory of TopKAT.<\/jats:p>","DOI":"10.1145\/3498690","type":"journal-article","created":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T17:03:12Z","timestamp":1642006992000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["On incorrectness logic and Kleene algebra with top and tests"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8197-6181","authenticated-orcid":false,"given":"Cheng","family":"Zhang","sequence":"first","affiliation":[{"name":"Boston University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arthur Azevedo","family":"de Amorim","sequence":"additional","affiliation":[{"name":"Boston University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marco","family":"Gaboardi","sequence":"additional","affiliation":[{"name":"Boston University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,1,12]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2578855.2535862"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00012-011-0142-3"},{"key":"e_1_2_2_3_1","unstructured":"Allegra Angus and Dexter Kozen. 2001. Kleene Algebra with Tests and Program Schematology. July https:\/\/ecommons.cornell.edu\/handle\/1813\/5831 Accepted: 2007-04-09T19:56:22Z Publisher: Cornell University.  Allegra Angus and Dexter Kozen. 2001. Kleene Algebra with Tests and Program Schematology. July https:\/\/ecommons.cornell.edu\/handle\/1813\/5831 Accepted: 2007-04-09T19:56:22Z Publisher: Cornell University."},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06251-8_7"},{"key":"e_1_2_2_5_1","unstructured":"Ernie Cohen Dexter Kozen and Frederick Smith. 1999. The Complexity of Kleene Algebra with Tests. July.  Ernie Cohen Dexter Kozen and Frederick Smith. 1999. The Complexity of Kleene Algebra with Tests. July."},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24690-6_12"},{"key":"e_1_2_2_7_1","unstructured":"Jules Desharnais Bernhard M\u00f6ller and Georg Struth. 2004. Modal Kleene Algebra and Applications \u2013 A Survey. In Journal on Relational Methods in Computer Science. 93\u2013131.  Jules Desharnais Bernhard M\u00f6ller and Georg Struth. 2004. Modal Kleene Algebra and Applications \u2013 A Survey. In Journal on Relational Methods in Computer Science. 93\u2013131."},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1183278.1183285"},{"key":"e_1_2_2_9_1","volume-title":"March, arxiv:2011.04704 arXiv","author":"Fahrenberg Uli","year":"2011","unstructured":"Uli Fahrenberg , Christian Johansen , Georg Struth , and Krzysztof Ziemi\u00e1nski . 2021. Domain Semirings United. arXiv:2011.04704 [cs] , March, arxiv:2011.04704 arXiv : 2011 .04704. Uli Fahrenberg, Christian Johansen, Georg Struth, and Krzysztof Ziemi\u00e1nski. 2021. Domain Semirings United. arXiv:2011.04704 [cs], March, arxiv:2011.04704 arXiv: 2011.04704."},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(79)90046-1"},{"key":"e_1_2_2_11_1","volume-title":"Mathematical Aspects of Computer Science","author":"Floyd Robert W.","unstructured":"Robert W. Floyd . 1967. Assigning Meanings to Programs . In Mathematical Aspects of Computer Science , J. T. Schwartz (Ed.) (Symposia in Applied Mathematics, Vol . 19). American Mathematical Society , Providence, RI. 19\u201332. Robert W. Floyd. 1967. Assigning Meanings to Programs. In Mathematical Aspects of Computer Science, J. T. Schwartz (Ed.) (Symposia in Applied Mathematics, Vol. 19). American Mathematical Society, Providence, RI. 19\u201332."},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48989-6_19"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1037"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/256167.256195"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/343369.343378"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44957-4_38"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63172-0_43"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00370681"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54458-7_6"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-88701-8_20"},{"key":"e_1_2_2_22_1","unstructured":"Toby Murray. 2020. An Under-Approximate Relational Logic. Archive of Formal Proofs Mar issn:2150-914x  Toby Murray. 2020. An Under-Approximate Relational Logic. Archive of Formal Proofs Mar issn:2150-914x"},{"key":"e_1_2_2_23_1","volume-title":"Equational Logic as a Programming Language","author":"O\u2019Donnell Michael J.","unstructured":"Michael J. O\u2019Donnell . 1985. Equational Logic as a Programming Language . The MIT Press . Michael J. O\u2019Donnell. 1985. Equational Logic as a Programming Language. The MIT Press."},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371078"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_15"},{"key":"e_1_2_2_26_1","unstructured":"Damien Pous. 2016. Automata for relation algebra and formal proofs. ENS Lyon. https:\/\/hal.archives-ouvertes.fr\/tel-01445821  Damien Pous. 2016. Automata for relation algebra and formal proofs. ENS Lyon. https:\/\/hal.archives-ouvertes.fr\/tel-01445821"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/800141.804649"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_14"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3093333.3009843"},{"key":"e_1_2_2_30_1","volume-title":"Universal Algebra","author":"Taylor Walter","unstructured":"Walter Taylor . 1979. Equational logic . In Universal Algebra ( second ed.), G. Gr\u00e4tzer (Ed.). Springer , New York. 378\u2013400. Walter Taylor. 1979. Equational logic. In Universal Algebra (second ed.), G. Gr\u00e4tzer (Ed.). Springer, New York. 378\u2013400."},{"key":"e_1_2_2_31_1","volume-title":"Arthur Azevedo de Amorim, and Marco Gaboardi","author":"Zhang Cheng","year":"2021","unstructured":"Cheng Zhang , Arthur Azevedo de Amorim, and Marco Gaboardi . 2021 . On Incorrectness Logic and Kleene Algebra With Top and Tests . arxiv:2108.07707. Cheng Zhang, Arthur Azevedo de Amorim, and Marco Gaboardi. 2021. On Incorrectness Logic and Kleene Algebra With Top and Tests. arxiv:2108.07707."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498690","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498690","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498690","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:30:28Z","timestamp":1750188628000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498690"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,12]]},"references-count":31,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2022,1,16]]}},"alternative-id":["10.1145\/3498690"],"URL":"https:\/\/doi.org\/10.1145\/3498690","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,1,12]]},"assertion":[{"value":"2022-01-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}