{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T20:59:44Z","timestamp":1760043584448,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":53,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,6,9]],"date-time":"2022-06-09T00:00:00Z","timestamp":1654732800000},"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":[],"published-print":{"date-parts":[[2022,6,9]]},"DOI":"10.1145\/3519939.3523722","type":"proceedings-article","created":{"date-parts":[[2022,6,2]],"date-time":"2022-06-02T21:05:05Z","timestamp":1654203905000},"page":"594-608","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Kleene algebra modulo theories: a framework for concrete KATs"],"prefix":"10.1145","author":[{"given":"Michael","family":"Greenberg","sequence":"first","affiliation":[{"name":"Stevens Institute of Technology, USA"}]},{"given":"Ryan","family":"Beckett","sequence":"additional","affiliation":[{"name":"Microsoft Research, USA"}]},{"given":"Eric","family":"Campbell","sequence":"additional","affiliation":[{"name":"Cornell University, USA"}]}],"member":"320","published-online":{"date-parts":[[2022,6,9]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535862"},{"key":"e_1_3_2_1_2_1","volume-title":"Kleene Algebra with Tests and Program Schematology","author":"Angus Allegra","year":"1813","unstructured":"Allegra Angus and Dexter Kozen . 2001. Kleene Algebra with Tests and Program Schematology . Cornell University , Ithaca, NY, USA . https:\/\/doi.org\/ 1813 \/5831 Allegra Angus and Dexter Kozen. 2001. Kleene Algebra with Tests and Program Schematology. Cornell University, Ithaca, NY, USA. https:\/\/doi.org\/1813\/5831"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360604"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2934872.2934892"},{"volume-title":"Planning with First-order Temporally Extended Goals Using Heuristic Search. In National Conference on Artificial Intelligence (AAAI\u201906)","author":"Jorge","key":"e_1_3_2_1_5_1","unstructured":"Jorge A. Baier and Sheila A. McIlraith. 2006 . Planning with First-order Temporally Extended Goals Using Heuristic Search. In National Conference on Artificial Intelligence (AAAI\u201906) . AAAI Press, 788\u2013795. isbn:978-1-57735-281-5 http:\/\/dl.acm.org\/citation.cfm?id=1597538.1597664 Jorge A. Baier and Sheila A. McIlraith. 2006. Planning with First-order Temporally Extended Goals Using Heuristic Search. In National Conference on Artificial Intelligence (AAAI\u201906). AAAI Press, 788\u2013795. isbn:978-1-57735-281-5 http:\/\/dl.acm.org\/citation.cfm?id=1597538.1597664"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1108768.1108813"},{"key":"e_1_3_2_1_7_1","volume-title":"Equational verification of cache blocking in LU decomposition using Kleene algebra with tests","author":"Barth Adam","year":"1813","unstructured":"Adam Barth and Dexter Kozen . 2002. Equational verification of cache blocking in LU decomposition using Kleene algebra with tests . Cornell University . https:\/\/hdl.handle.net\/ 1813 \/5848 Adam Barth and Dexter Kozen. 2002. Equational verification of cache blocking in LU decomposition using Kleene algebra with tests. Cornell University. https:\/\/hdl.handle.net\/1813\/5848"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908108"},{"key":"e_1_3_2_1_9_1","unstructured":"Eric Campbell and Michael Greenberg. 2021. Injecting Finiteness to Prove Completeness for Finite Linear Temporal Logic. CoRR arXiv:2107.06045.  Eric Campbell and Michael Greenberg. 2021. Injecting Finiteness to Prove Completeness for Finite Linear Temporal Logic. CoRR arXiv:2107.06045."},{"volume-title":"Infiniteness and Linear Temporal Logic: Soundness, Completeness, and Decidability","author":"Campbell Eric Hayden","key":"e_1_3_2_1_10_1","unstructured":"Eric Hayden Campbell . 2017. Infiniteness and Linear Temporal Logic: Soundness, Completeness, and Decidability . Pomona College . Eric Hayden Campbell. 2017. Infiniteness and Linear Temporal Logic: Soundness, Completeness, and Decidability. Pomona College."},{"key":"e_1_3_2_1_11_1","unstructured":"Ernie Cohen. 1994. Hypotheses in Kleene Algebra. http:\/\/citeseerx.ist.psu.edu\/viewdoc\/summary?doi=10.1.1.56.6067  Ernie Cohen. 1994. Hypotheses in Kleene Algebra. http:\/\/citeseerx.ist.psu.edu\/viewdoc\/summary?doi=10.1.1.56.6067"},{"key":"e_1_3_2_1_12_1","unstructured":"Ernie Cohen. 1994. Lazy Caching in Kleene Algebra. http:\/\/citeseerx.ist.psu.edu\/viewdoc\/summary?doi=10.1.1.57.5074  Ernie Cohen. 1994. Lazy Caching in Kleene Algebra. http:\/\/citeseerx.ist.psu.edu\/viewdoc\/summary?doi=10.1.1.57.5074"},{"key":"e_1_3_2_1_13_1","unstructured":"Ernie Cohen. 1994. Using Kleene algebra to reason about concurrency control. Telcordia.  Ernie Cohen. 1994. Using Kleene algebra to reason about concurrency control. Telcordia."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/343369.343404"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66902-1_16"},{"key":"e_1_3_2_1_16_1","volume-title":"Riccardo De Masellis, and Marco Montali","author":"Giacomo Giuseppe De","year":"2014","unstructured":"Giuseppe De Giacomo , Riccardo De Masellis, and Marco Montali . 2014 . Reasoning on LTL on Finite Traces : Insensitivity to Infiniteness.. In AAAI. 1027\u20131033. https:\/\/www.diag.uniroma1.it\/degiacom\/papers\/2014\/AAAI14.pdf Giuseppe De Giacomo, Riccardo De Masellis, and Marco Montali. 2014. Reasoning on LTL on Finite Traces: Insensitivity to Infiniteness.. In AAAI. 1027\u20131033. https:\/\/www.diag.uniroma1.it\/degiacom\/papers\/2014\/AAAI14.pdf"},{"key":"e_1_3_2_1_17_1","volume-title":"IJCAI\u201913 Proceedings of the Twenty-Third international joint conference on Artificial Intelligence. 854\u2013860","author":"Giacomo Giuseppe De","year":"2013","unstructured":"Giuseppe De Giacomo and Moshe Y Vardi . 2013 . Linear temporal logic and linear dynamic logic on finite traces . In IJCAI\u201913 Proceedings of the Twenty-Third international joint conference on Artificial Intelligence. 854\u2013860 . https:\/\/www.ijcai.org\/Proceedings\/13\/Papers\/132.pdf Giuseppe De Giacomo and Moshe Y Vardi. 2013. Linear temporal logic and linear dynamic logic on finite traces. In IJCAI\u201913 Proceedings of the Twenty-Third international joint conference on Artificial Intelligence. 854\u2013860. https:\/\/www.ijcai.org\/Proceedings\/13\/Papers\/132.pdf"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1995376.1995394"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034812"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_12"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677011"},{"key":"e_1_3_2_1_24_1","volume-title":"Furia and Bertrand Meyer","author":"Carlo","year":"2009","unstructured":"Carlo A. Furia and Bertrand Meyer . 2009 . Inferring Loop Invariants using Postconditions. CoRR , arXiv:0909.0884. Carlo A. Furia and Bertrand Meyer. 2009. Inferring Loop Invariants using Postconditions. CoRR, arXiv:0909.0884."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15025-8_15"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19805-2_25"},{"key":"e_1_3_2_1_27_1","volume-title":"Eva May, Gordon Fraser, and Andreas Zeller.","author":"Galeotti Juan P.","year":"2014","unstructured":"Juan P. Galeotti , Carlo A. Furia , Eva May, Gordon Fraser, and Andreas Zeller. 2014 . Automating Full Functional Verification of Programs with Loops. CoRR , arXiv:1407.5286. Juan P. Galeotti, Carlo A. Furia, Eva May, Gordon Fraser, and Andreas Zeller. 2014. Automating Full Functional Verification of Programs with Loops. CoRR, arXiv:1407.5286."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603095"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462178"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17164-2_23"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/256167.256195"},{"key":"e_1_3_2_1_32_1","volume-title":"Kleene algebra with tests and the static analysis of programs","author":"Kozen Dexter","year":"1813","unstructured":"Dexter Kozen . 2003. Kleene algebra with tests and the static analysis of programs . Cornell University . https:\/\/hdl.handle.net\/ 1813 \/5627 Dexter Kozen. 2003. Kleene algebra with tests and the static analysis of programs. Cornell University. https:\/\/hdl.handle.net\/1813\/5627"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2003.09.004"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-47843-2_15"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43951-7_24"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44957-4_38"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.OPODIS.2016.18"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908097"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103685"},{"key":"e_1_3_2_1_40_1","first-page":"1","article-title":"Decision Methods for Concurrent Kleene Algebra with Tests: Based on Derivative","volume":"2015","author":"Nakamura Yoshiki","year":"2015","unstructured":"Yoshiki Nakamura . 2015 . Decision Methods for Concurrent Kleene Algebra with Tests: Based on Derivative . RAMiCS 2015 , 1 . http:\/\/ceur-ws.org\/Vol-1454\/ramics15-st_1-8.pdf Yoshiki Nakamura. 2015. Decision Methods for Concurrent Kleene Algebra with Tests: Based on Derivative. RAMiCS 2015, 1. http:\/\/ceur-ws.org\/Vol-1454\/ramics15-st_1-8.pdf","journal-title":"RAMiCS"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/357073.357079"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908099"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677007"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491185.2491187"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-018-0321-3"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00056-6"},{"key":"e_1_3_2_1_47_1","unstructured":"Andrew E. Santosa. 2015. Comparing Weakest Precondition and Weakest Liberal Precondition. CoRR arXiv:1512.04013.  Andrew E. Santosa. 2015. Comparing Weakest Precondition and Weakest Liberal Precondition. CoRR arXiv:1512.04013."},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2692915.2628157"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0248-5"},{"key":"e_1_3_2_1_50_1","unstructured":"Alexandra Silva. 2010. Kleene Coalgebra. University of Minho. Braga Portugal. https:\/\/alexandrasilva.org\/files\/thesis.pdf  Alexandra Silva. 2010. Kleene Coalgebra. University of Minho. Braga Portugal. https:\/\/alexandrasilva.org\/files\/thesis.pdf"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784761"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371129"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2001.932480"}],"event":{"name":"PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"San Diego CA USA","acronym":"PLDI '22"},"container-title":["Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3519939.3523722","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3519939.3523722","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:10:30Z","timestamp":1750183830000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3519939.3523722"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,6,9]]},"references-count":53,"alternative-id":["10.1145\/3519939.3523722","10.1145\/3519939"],"URL":"https:\/\/doi.org\/10.1145\/3519939.3523722","relation":{},"subject":[],"published":{"date-parts":[[2022,6,9]]},"assertion":[{"value":"2022-06-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}