{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,15]],"date-time":"2026-01-15T11:56:53Z","timestamp":1768478213950,"version":"3.49.0"},"reference-count":46,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T00:00:00Z","timestamp":1576800000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100011199","name":"European Research Council","doi-asserted-by":"publisher","award":["679127"],"award-info":[{"award-number":["679127"]}],"id":[{"id":"10.13039\/100011199","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Leverhulme Prize","award":["PLP-2016-129"],"award-info":[{"award-number":["PLP-2016-129"]}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["AitF-1637532, CNS-1413978, and SaTC-1717581"],"award-info":[{"award-number":["AitF-1637532, CNS-1413978, and SaTC-1717581"]}],"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":[[2020,1]]},"abstract":"<jats:p>Guarded Kleene Algebra with Tests (GKAT) is a variation on Kleene Algebra with Tests (KAT) that arises by restricting the union (+) and iteration (*) operations from KAT to predicate-guarded versions. We develop the (co)algebraic theory of GKAT and show how it can be efficiently used to reason about imperative programs. In contrast to KAT, whose equational theory is PSPACE-complete, we show that the equational theory of GKAT is (almost) linear time. We also provide a full Kleene theorem and prove completeness for an analogue of Salomaa\u2019s axiomatization of Kleene Algebra.<\/jats:p>","DOI":"10.1145\/3371129","type":"journal-article","created":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T19:45:25Z","timestamp":1576871125000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":26,"title":["Guarded Kleene algebra with tests: verification of uninterpreted programs in nearly linear time"],"prefix":"10.1145","volume":"4","author":[{"given":"Steffen","family":"Smolka","sequence":"first","affiliation":[{"name":"Cornell University, USA"}]},{"given":"Nate","family":"Foster","sequence":"additional","affiliation":[{"name":"Cornell University, USA"}]},{"given":"Justin","family":"Hsu","sequence":"additional","affiliation":[{"name":"University of Wisconsin-Madison, USA"}]},{"given":"Tobias","family":"Kapp\u00e9","sequence":"additional","affiliation":[{"name":"University College London, UK"}]},{"given":"Dexter","family":"Kozen","sequence":"additional","affiliation":[{"name":"Cornell University, USA"}]},{"given":"Alexandra","family":"Silva","sequence":"additional","affiliation":[{"name":"University College London, UK"}]}],"member":"320","published-online":{"date-parts":[[2019,12,20]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535862"},{"key":"e_1_2_1_3_1","volume-title":"Proc. Information Processing (IFIP)","volume":"1","author":"Edward"},{"key":"e_1_2_1_6_1","volume-title":"Bartee","author":"Birkhoff Garrett","year":"1970"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/355592.365646"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429124"},{"key":"e_1_2_1_9_1","unstructured":"Ernie Cohen. 1994a. Lazy Caching in Kleene Algebra.  Ernie Cohen. 1994a. Lazy Caching in Kleene Algebra."},{"key":"e_1_2_1_12_1","volume-title":"Regular Algebra and Finite Machines","author":"Conway John Horton"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCL.1994.288377"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(79)90046-1"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_12"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677011"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(73)80040-6"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0092872"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57502-2_61"},{"key":"e_1_2_1_20_1","volume-title":"Karp","author":"Hopcroft John E.","year":"1971"},{"key":"e_1_2_1_21_1","volume-title":"The Logical Schemes of Algorithms. Problems of Cybernetics","author":"Ianov I.","year":"1960"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(69)80027-9"},{"key":"e_1_2_1_23_1","volume-title":"Representation of Events in Nerve Nets and Finite Automata. Automata Studies","author":"Kleene Stephen C.","year":"1956"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/800125.804055"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61042-1_35"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/256167.256195"},{"key":"e_1_2_1_27_1","volume-title":"Automata on Guarded Strings and Applications. Mat\u00e9matica Contempor\u00e2nea 24","author":"Kozen Dexter","year":"2003"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.32"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44957-4_38"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63172-0_43"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70594-9_11"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(70)80022-8"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.12.113"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1002\/(SICI)1096-908X(199701)9:1%26#38;lt;47::AID-SMR142%26#38;gt;3.0.CO;2-V"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/357073.357079"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/25.3.379"},{"key":"e_1_2_1_37_1","volume-title":"Record of Project MAC Conference on Concurrent Systems and Parallel Computation. ACM","author":"Michael"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/355609.362337"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677007"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/48014.48021"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/321203.321204"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00056-6"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/321312.321326"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/321160.321170"},{"key":"e_1_2_1_45_1","unstructured":"Alexandra Silva. 2010. Kleene Coalgebra. Ph.D. Dissertation. Radboud University.  Alexandra Silva. 2010. Kleene Coalgebra. Ph.D. Dissertation. Radboud University."},{"key":"e_1_2_1_46_1","volume-title":"Guarded Kleene Algebra with Tests: Verification of Uninterpreted Programs in Nearly Linear Time (Extended Version). arXiv","author":"Smolka Steffen","year":"1907"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314639"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/321879.321884"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/363347.363387"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129505005074"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/21.2.161"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371129","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371129","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371129","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:05:43Z","timestamp":1750273543000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371129"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12,20]]},"references-count":46,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2020,1]]}},"alternative-id":["10.1145\/3371129"],"URL":"https:\/\/doi.org\/10.1145\/3371129","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,12,20]]},"assertion":[{"value":"2019-12-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}