{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T22:48:24Z","timestamp":1775861304063,"version":"3.50.1"},"publisher-location":"Cham","reference-count":53,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032227225","type":"print"},{"value":"9783032227232","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-22723-2_14","type":"book-chapter","created":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T12:01:25Z","timestamp":1775822485000},"page":"392-423","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Outrunning Big KATs: Efficient Decision Procedures for Variants of GKAT"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8197-6181","authenticated-orcid":false,"given":"Cheng","family":"Zhang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5234-8565","authenticated-orcid":false,"given":"Qiancheng","family":"Fu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hang","family":"Ji","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ines Santacruz Del","family":"Valle","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5014-9784","authenticated-orcid":false,"given":"Alexandra","family":"Silva","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5235-7066","authenticated-orcid":false,"given":"Marco","family":"Gaboardi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,4,10]]},"reference":[{"key":"14_CR1","doi-asserted-by":"publisher","unstructured":"Almeida, R., Broda, S., Moreira, N.: Deciding KAT and Hoare Logic with Derivatives. Electronic Proceedings in Theoretical Computer Science 96, 127\u2013140 (Oct 2012), ISSN 2075-2180, https:\/\/doi.org\/10.4204\/EPTCS.96.10","DOI":"10.4204\/EPTCS.96.10"},{"key":"14_CR2","doi-asserted-by":"publisher","unstructured":"Anderson, C.J., Foster, N., Guha, A., Jeannin, J.B., Kozen, D., Schlesinger, C., Walker, D.: NetKAT: Semantic foundations for networks. ACM SIGPLAN Notices 49(1), 113\u2013126 (Jan 2014), ISSN 0362-1340, https:\/\/doi.org\/10.1145\/2578855.2535862","DOI":"10.1145\/2578855.2535862"},{"key":"14_CR3","unstructured":"Angus, A., Kozen, D.: Kleene Algebra with Tests and Program Schematology. Technical Report, Cornell University, USA (Jun 2001)"},{"key":"14_CR4","doi-asserted-by":"publisher","unstructured":"Antimirov, V.: Partial derivatives of regular expressions and finite automaton constructions. Theoretical Computer Science 155(2), 291\u2013319 (Mar 1996), ISSN 03043975, https:\/\/doi.org\/10.1016\/0304-3975(95)00182-4","DOI":"10.1016\/0304-3975(95)00182-4"},{"key":"14_CR5","doi-asserted-by":"publisher","unstructured":"Bonchi, F., Petri\u015fan, D., Pous, D., Rot, J.: A general account of coinduction up-to. Acta Informatica 54(2), 127\u2013190 (Mar 2017), ISSN 0001-5903, 1432-0525, https:\/\/doi.org\/10.1007\/s00236-016-0271-4","DOI":"10.1007\/s00236-016-0271-4"},{"key":"14_CR6","unstructured":"BooleWorks GmbH: Booleworks\/logicng-rs (Jan 2025), https:\/\/github.com\/booleworks\/logicng-rs"},{"key":"14_CR7","doi-asserted-by":"publisher","unstructured":"Bryant: Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers C-35(8), 677\u2013691 (1986), https:\/\/doi.org\/10.1109\/TC.1986.1676819","DOI":"10.1109\/TC.1986.1676819"},{"key":"14_CR8","doi-asserted-by":"publisher","unstructured":"Brzozowski, J.A.: Derivatives of Regular Expressions. Journal of the ACM 11(4), 481\u2013494 (Oct 1964), ISSN 0004-5411, https:\/\/doi.org\/10.1145\/321239.321249","DOI":"10.1145\/321239.321249"},{"key":"14_CR9","unstructured":"Cohen, E., Kozen, D., Smith, F.: The Complexity of Kleene Algebra with Tests (Jul 1996)"},{"key":"14_CR10","doi-asserted-by":"publisher","unstructured":"Dalla\u00a0Preda, M., Giacobazzi, R., Lakhotia, A., Mastroeni, I.: Abstract Symbolic Automata: Mixed syntactic\/semantic similarity analysis of executables. In: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 329\u2013341, ACM, Mumbai India (Jan 2015), ISBN 978-1-4503-3300-9, https:\/\/doi.org\/10.1145\/2676726.2676986","DOI":"10.1145\/2676726.2676986"},{"key":"14_CR11","doi-asserted-by":"publisher","unstructured":"Deifel, H.P., Milius, S., Schr\u00f6der, L., Wi\u00dfmann, T.: Generic Partition Refinement and Weighted Tree Automata. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) Formal Methods \u2013 The Next 30 Years, pp. 280\u2013297, Springer International Publishing, Cham (2019), ISBN 978-3-030-30942-https:\/\/doi.org\/10.1007\/978-3-030-30942-8_18","DOI":"10.1007\/978-3-030-30942-8_18"},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"Desharnais, J., M\u00f6ller, B., Struth, G.: Modal Kleene Algebra and Applications \u2013 A Survey. In: Journal on Relational Methods in Computer Science, pp. 93\u2013131 (2004)","DOI":"10.1007\/978-3-540-24771-5_2"},{"key":"14_CR13","doi-asserted-by":"publisher","unstructured":"Erosa, A., Hendren, L.: Taming control flow: A structured approach to eliminating goto statements. In: Proceedings of 1994 IEEE International Conference on Computer Languages (ICCL\u201994), pp. 229\u2013240 (May 1994), https:\/\/doi.org\/10.1109\/ICCL.1994.288377","DOI":"10.1109\/ICCL.1994.288377"},{"key":"14_CR14","doi-asserted-by":"publisher","unstructured":"Fernandez, J.C., Mounier, L., Jard, C., J\u00e9ron, T.: On-the-fly verification of finite transition systems. Formal Methods in System Design 1(2), 251\u2013273 (Oct 1992), ISSN 1572-8102, https:\/\/doi.org\/10.1007\/BF00121127","DOI":"10.1007\/BF00121127"},{"key":"14_CR15","doi-asserted-by":"publisher","unstructured":"Foster, N., Kozen, D., Milano, M., Silva, A., Thompson, L.: A Coalgebraic Decision Procedure for NetKAT. In: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 343\u2013355, POPL \u201915, Association for Computing Machinery, New York, NY, USA (Jan 2015), ISBN 978-1-4503-3300-9, https:\/\/doi.org\/10.1145\/2676726.2677011","DOI":"10.1145\/2676726.2677011"},{"key":"14_CR16","doi-asserted-by":"publisher","unstructured":"Fu, Q., Zhang, C., Ji, H., Santacruz Del\u00a0Valle, I., Silva, A., Gaboardi, M.: Efficient Decision Procedures for Variants of GKAT (Artifact) (2026), https:\/\/doi.org\/10.5281\/zenodo.18304183, https:\/\/zenodo.org\/records\/18304183","DOI":"10.5281\/zenodo.18304183"},{"key":"14_CR17","unstructured":"GNU Project: Coreutils - GNU core utilities (2024), https:\/\/www.gnu.org\/software\/coreutils\/"},{"key":"14_CR18","unstructured":"Gomes, L., Baillot, P., Gaboardi, M.: A Kleene algebra with tests for union bound reasoning about probabilistic programs (Jul 2024)"},{"key":"14_CR19","doi-asserted-by":"publisher","unstructured":"Hoare, C., M\u00f6ller, B., Struth, G., Wehrman, I.: Concurrent Kleene Algebra. vol. 5710, pp. 399\u2013414 (Sep 2009), ISBN 978-3-642-04080-1, https:\/\/doi.org\/10.1007\/978-3-642-04081-8_27","DOI":"10.1007\/978-3-642-04081-8_27"},{"key":"14_CR20","unstructured":"Hopcroft, J.E., Karp, R.M.: A Linear Algorithm for Testing Equivalence of Finite Automata. Tech. rep., Cornell University (Dec 1971)"},{"key":"14_CR21","doi-asserted-by":"publisher","unstructured":"Kozen, D.: On the Coalgebraic Theory of Kleene Algebra with Tests. In: Ba\u015fkent, C., Moss, L.S., Ramanujam, R. (eds.) Rohit Parikh on Logic, Language and Society, pp. 279\u2013298, Outstanding Contributions to Logic, Springer International Publishing, Cham (2017), ISBN 978-3-319-47843-2, https:\/\/doi.org\/10.1007\/978-3-319-47843-2_15","DOI":"10.1007\/978-3-319-47843-2_15"},{"key":"14_CR22","doi-asserted-by":"publisher","unstructured":"Kozen, D., Patron, M.C.: Certification of Compiler Optimizations Using Kleene Algebra with Tests. In: Lloyd, J., Dahl, V., Furbach, U., Kerber, M., Lau, K.K., Palamidessi, C., Pereira, L.M., Sagiv, Y., Stuckey, P.J. (eds.) Computational Logic \u2014 CL 2000, pp. 568\u2013582, Lecture Notes in Computer Science, Springer, Berlin, Heidelberg (2000), ISBN 978-3-540-44957-7, https:\/\/doi.org\/10.1007\/3-540-44957-4_38","DOI":"10.1007\/3-540-44957-4_38"},{"key":"14_CR23","doi-asserted-by":"publisher","unstructured":"Kozen, D., Smith, F.: Kleene algebra with tests: Completeness and decidability. In: Goos, G., Hartmanis, J., Leeuwen, J., Dalen, D., Bezem, M. (eds.) Computer Science Logic, vol. 1258, pp. 244\u2013259, Springer Berlin Heidelberg, Berlin, Heidelberg (1997), ISBN 978-3-540-63172-9 978-3-540-69201-0, https:\/\/doi.org\/10.1007\/3-540-63172-0_43","DOI":"10.1007\/3-540-63172-0_43"},{"key":"14_CR24","doi-asserted-by":"publisher","unstructured":"Kozen, D., Tseng, W.L.D.: The B\u00f6hm\u2013Jacopini Theorem Is False, Propositionally. In: Audebaud, P., Paulin-Mohring, C. (eds.) Mathematics of Program Construction, vol. 5133, pp. 177\u2013192, Springer Berlin Heidelberg, Berlin, Heidelberg (2008), ISBN 978-3-540-70593-2 978-3-540-70594-9, https:\/\/doi.org\/10.1007\/978-3-540-70594-9_11","DOI":"10.1007\/978-3-540-70594-9_11"},{"key":"14_CR25","unstructured":"Lewis, P.: Pclewis\/cudd-sys (Apr 2025), https:\/\/github.com\/pclewis\/cudd-sys"},{"key":"14_CR26","unstructured":"llvm: LLVM $$\\cdot $$ llvm\/llvm-project (2025), https:\/\/github.com\/llvm\/llvm-project\/releases\/tag\/llvmorg-20.1.2"},{"key":"14_CR27","doi-asserted-by":"publisher","unstructured":"Moeller, M., Jacobs, J., Belanger, O.S., Darais, D., Schlesinger, C., Smolka, S., Foster, N., Silva, A.: KATch: A Fast Symbolic Verifier for NetKAT. KATch: A Fast Symbolic Verifier for NetKAT 8(PLDI), 224:1905\u2013224:1928 (Jun 2024), https:\/\/doi.org\/10.1145\/3656454","DOI":"10.1145\/3656454"},{"key":"14_CR28","doi-asserted-by":"publisher","unstructured":"Moeller, M., Jacobs, J., Belanger, O.S., Darais, D., Schlesinger, C., Smolka, S., Foster, N., Silva, A.: Katch: A fast symbolic verifier for netkat (2024), https:\/\/doi.org\/10.5281\/zenodo.10961123","DOI":"10.5281\/zenodo.10961123"},{"key":"14_CR29","unstructured":"NationalSecurityAgency: Ghidra. GitHub (2025), https:\/\/github.com\/NationalSecurityAgency\/ghidra"},{"key":"14_CR30","doi-asserted-by":"publisher","unstructured":"Owens, S., Reppy, J., Turon, A.: Regular-expression derivatives re-examined 19(2), 173\u2013190 (2009), ISSN 1469-7653, 0956-7968, https:\/\/doi.org\/10.1017\/S0956796808007090, https:\/\/www.cambridge.org\/core\/journals\/journal-of-functional-programming\/article\/regularexpression-derivatives-reexamined\/E5734B86DEB96C61C69E5CF3C4FB0AFA","DOI":"10.1017\/S0956796808007090"},{"key":"14_CR31","doi-asserted-by":"publisher","unstructured":"Pous, D.: Complete Lattices and Up-To Techniques. In: Hutchison, D., Kanade, T., Kittler, J., Kleinberg, J.M., Mattern, F., Mitchell, J.C., Naor, M., Nierstrasz, O., Pandu\u00a0Rangan, C., Steffen, B., Sudan, M., Terzopoulos, D., Tygar, D., Vardi, M.Y., Weikum, G., Shao, Z. (eds.) Programming Languages and Systems, vol. 4807, pp. 351\u2013366, Springer Berlin Heidelberg, Berlin, Heidelberg (2007), ISBN 978-3-540-76636-0 978-3-540-76637-7, https:\/\/doi.org\/10.1007\/978-3-540-76637-7_24","DOI":"10.1007\/978-3-540-76637-7_24"},{"key":"14_CR32","doi-asserted-by":"publisher","unstructured":"Pous, D.: Symbolic Algorithms for Language Equivalence and Kleene Algebra with Tests. In: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 357\u2013368, POPL \u201915, Association for Computing Machinery, New York, NY, USA (Jan 2015), ISBN 978-1-4503-3300-9, https:\/\/doi.org\/10.1145\/2676726.2677007","DOI":"10.1145\/2676726.2677007"},{"key":"14_CR33","unstructured":"Qiancheng Fu: Possible bug in decompiler \"join\" label gotos? $$\\cdot $$ issue #8310 of NationalSecurityAgency\/ghidra (2025), https:\/\/github.com\/NationalSecurityAgency\/ghidra\/issues\/8310"},{"key":"14_CR34","doi-asserted-by":"publisher","unstructured":"R\u00f3\u017cowski, W., Kapp\u00e9, T., Kozen, D., Schmid, T., Silva, A.: Probabilistic Guarded KAT Modulo Bisimilarity: Completeness and Complexity. In: Etessami, K., Feige, U., Puppis, G. (eds.) 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023), Leibniz International Proceedings in Informatics (LIPIcs), vol. 261, pp. 136:1\u2013136:20, Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2023), ISBN 978-3-95977-278-5, ISSN 1868-8969, https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2023.136","DOI":"10.4230\/LIPIcs.ICALP.2023.136"},{"key":"14_CR35","doi-asserted-by":"publisher","unstructured":"Saarikivi, O., Veanes, M., Mytkowicz, T., Musuvathi, M.: Fusing effectful comprehensions. In: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 17\u201332, ACM, Barcelona Spain (Jun 2017), ISBN 978-1-4503-4988-8, https:\/\/doi.org\/10.1145\/3062341.3062362","DOI":"10.1145\/3062341.3062362"},{"key":"14_CR36","doi-asserted-by":"publisher","unstructured":"Schmid, T., Kapp\u00e9, T., Kozen, D., Silva, A.: Guarded Kleene Algebra with Tests: Coequations, Coinduction, and Completeness. In: Bansal, N., Merelli, E., Worrell, J. (eds.) 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021), Leibniz International Proceedings in Informatics (LIPIcs), vol. 198, pp. 142:1\u2013142:14, Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2021), ISBN 978-3-95977-195-5, ISSN 1868-8969, https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2021.142","DOI":"10.4230\/LIPIcs.ICALP.2021.142"},{"key":"14_CR37","unstructured":"Schmid, T.J.W.: Coalgebraic Completeness Theorems for Effectful Process Algebras. Doctoral, UCL (University College London) (Jan 2024)"},{"key":"14_CR38","doi-asserted-by":"publisher","unstructured":"Smolka, S., Foster, N., Hsu, J., Kapp\u00e9, T., Kozen, D., Silva, A.: Guarded Kleene algebra with tests: Verification of uninterpreted programs in nearly linear time. Proceedings of the ACM on Programming Languages 4(POPL), 1\u201328 (Jan 2020), ISSN 2475-1421, https:\/\/doi.org\/10.1145\/3371129","DOI":"10.1145\/3371129"},{"key":"14_CR39","doi-asserted-by":"publisher","unstructured":"Smolka, S., Kumar, P., Foster, N., Kozen, D., Silva, A.: Cantor meets Scott: Semantic foundations for probabilistic networks. ACM SIGPLAN Notices 52(1), 557\u2013571 (Jan 2017), ISSN 0362-1340, https:\/\/doi.org\/10.1145\/3093333.3009843","DOI":"10.1145\/3093333.3009843"},{"key":"14_CR40","doi-asserted-by":"publisher","unstructured":"Smolka, S., Kumar, P., Kahn, D.M., Foster, N., Hsu, J., Kozen, D., Silva, A.: Scalable verification of probabilistic networks. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 190\u2013203, ACM, Phoenix AZ USA (Jun 2019), ISBN 978-1-4503-6712-7, https:\/\/doi.org\/10.1145\/3314221.3314639","DOI":"10.1145\/3314221.3314639"},{"key":"14_CR41","unstructured":"Somenzi, F.: CUDD: CU Decision Diagram Package Release 2.7.0 (Jun 2018), https:\/\/add-lib.scce.info\/assets\/doxygen-cudd-documentation\/"},{"key":"14_CR42","doi-asserted-by":"publisher","unstructured":"Stanford, C., Veanes, M., Bj\u00f8rner, N.: Symbolic Boolean derivatives for efficiently solving extended regular expression constraints. In: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, pp. 620\u2013635, PLDI 2021, Association for Computing Machinery, New York, NY, USA (Jun 2021), ISBN 978-1-4503-8391-2, https:\/\/doi.org\/10.1145\/3453483.3454066","DOI":"10.1145\/3453483.3454066"},{"key":"14_CR43","doi-asserted-by":"publisher","unstructured":"Van\u00a0Koevering, S., R\u00f3\u017cowski, W., Silva, A.: Weighted GKAT: Completeness and Complexity 334, 172:1\u2013172:18 (2025), ISSN 1868-8969, https:\/\/doi.org\/10.4230\/LIPICS.ICALP.2025.172, https:\/\/drops.dagstuhl.de\/entities\/document\/10.4230\/LIPIcs.ICALP.2025.172","DOI":"10.4230\/LIPICS.ICALP.2025.172"},{"key":"14_CR44","doi-asserted-by":"publisher","unstructured":"Veanes, M.: Applications of Symbolic Finite Automata. In: Hutchison, D., Kanade, T., Kittler, J., Kleinberg, J.M., Mattern, F., Mitchell, J.C., Naor, M., Nierstrasz, O., Pandu\u00a0Rangan, C., Steffen, B., Sudan, M., Terzopoulos, D., Tygar, D., Vardi, M.Y., Weikum, G., Konstantinidis, S. (eds.) Implementation and Application of Automata, vol. 7982, pp. 16\u201323, Springer Berlin Heidelberg, Berlin, Heidelberg (2013), ISBN 978-3-642-39273-3 978-3-642-39274-0, https:\/\/doi.org\/10.1007\/978-3-642-39274-0_3","DOI":"10.1007\/978-3-642-39274-0_3"},{"key":"14_CR45","doi-asserted-by":"publisher","unstructured":"Veanes, M., Hooimeijer, P., Livshits, B., Molnar, D., Bjorner, N.: Symbolic finite state transducers: Algorithms and applications. SIGPLAN Not. 47(1), 137\u2013150 (Jan 2012), ISSN 0362-1340, https:\/\/doi.org\/10.1145\/2103621.2103674","DOI":"10.1145\/2103621.2103674"},{"key":"14_CR46","doi-asserted-by":"publisher","unstructured":"Wagemaker, J., Brunet, P., Docherty, S., Kapp\u00e9, T., Rot, J., Silva, A.: Partially Observable Concurrent Kleene Algebra. LIPIcs, Volume 171, CONCUR 2020 171, 20:1\u201320:22 (2020), ISSN 1868-8969, https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2020.20","DOI":"10.4230\/LIPIcs.CONCUR.2020.20"},{"key":"14_CR47","unstructured":"Wasserstein, J.: GUARDED NETKAT: SOUNDNESS, PARTIAL-COMPLETENESS, DECIDABILITY. Master of Science, Cornell Univerisity, Ithaca, NY (May 2023)"},{"key":"14_CR48","doi-asserted-by":"publisher","unstructured":"Yakdan, K., Eschweiler, S., Gerhards-Padilla, E., Smith, M.: No More Gotos: Decompilation Using Pattern-Independent Control-Flow Structuring and Semantics-Preserving Transformations. In: Proceedings 2015 Network and Distributed System Security Symposium, Internet Society, San Diego, CA (2015), ISBN 978-1-891562-38-9, https:\/\/doi.org\/10.14722\/ndss.2015.23185","DOI":"10.14722\/ndss.2015.23185"},{"key":"14_CR49","doi-asserted-by":"publisher","unstructured":"Zhang, C., de Amorim, A.A., Gaboardi, M.: On Incorrectness Logic and Kleene Algebra with Top and Tests (Aug 2022), https:\/\/doi.org\/10.48550\/arXiv.2108.07707","DOI":"10.48550\/arXiv.2108.07707"},{"key":"14_CR50","doi-asserted-by":"publisher","unstructured":"Zhang, C., de Amorim, A.A., Gaboardi, M.: Domain Reasoning in TopKAT (Apr 2024), https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2024.133","DOI":"10.4230\/LIPIcs.ICALP.2024.133"},{"key":"14_CR51","doi-asserted-by":"publisher","unstructured":"Zhang, C., Fu, Q., Ji, H., Valle, I.S.D., Silva, A., Gaboardi, M.: Outrunning Big KATs: Efficient Decision Procedures for Variants of GKAT (2026), https:\/\/doi.org\/10.48550\/arXiv.2601.09986","DOI":"10.48550\/arXiv.2601.09986"},{"key":"14_CR52","doi-asserted-by":"crossref","unstructured":"Zhang, C., Kapp\u00e9, T., Narv\u00e1ez, D.E., Naus, N.: CF-GKAT: Efficient Validation of Control-Flow Transformations. Proceedings of the ACM on Programming Languages (POPL) (2025)","DOI":"10.1145\/3704857"},{"key":"14_CR53","doi-asserted-by":"publisher","unstructured":"Zhang, C., Kapp\u00e9, T., Narva\u00e9z, D.E., Naus, N.: Cf-gkat: Efficient validation of control-flow transformations (artifact) (Oct 2024), https:\/\/doi.org\/10.5281\/zenodo.13938565, https:\/\/doi.org\/10.5281\/zenodo.13938565","DOI":"10.5281\/zenodo.13938565"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-22723-2_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T22:02:37Z","timestamp":1775858557000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-22723-2_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032227225","9783032227232"],"references-count":53,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-22723-2_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"10 April 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Turin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 April 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"35","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/about\/esop\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}