{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,19]],"date-time":"2026-05-19T14:53:25Z","timestamp":1779202405645,"version":"3.51.4"},"reference-count":52,"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":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["2040249,1845803,2234257"],"award-info":[{"award-number":["2040249,1845803,2234257"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100010661","name":"Horizon 2020 Framework Programme","doi-asserted-by":"publisher","award":["101027412"],"award-info":[{"award-number":["101027412"]}],"id":[{"id":"10.13039\/100010661","id-type":"DOI","asserted-by":"publisher"}]},{"name":"National Research Council of the Netherlands","award":["VI.Veni.232.286"],"award-info":[{"award-number":["VI.Veni.232.286"]}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["N66001-21-C-4028"],"award-info":[{"award-number":["N66001-21-C-4028"]}],"id":[{"id":"10.13039\/100000185","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":[[2025,1,7]]},"abstract":"<jats:p>\n                    Guarded Kleene Algebra with Tests (GKAT) provides a sound and complete framework to reason about trace equivalence between simple imperative programs. However, there are still several notable limitations. First, GKAT is completely agnostic with respect to the meaning of primitives, to keep equivalence decidable. Second, GKAT excludes non-local control flow such as\n                    <jats:monospace>goto, break<\/jats:monospace>\n                    , and\n                    <jats:monospace>return<\/jats:monospace>\n                    . To overcome these limitations, we introduce\n                    <jats:italic toggle=\"yes\">Control-Flow GKAT (CF-GKAT)<\/jats:italic>\n                    , a system that allows reasoning about programs that include non-local control flow as well as hardcoded values. CF-GKAT is able to soundly and completely verify trace equivalence of a larger class of programs, while preserving the nearly-linear efficiency of GKAT. This makes CF-GKAT suitable for the verification of control-flow manipulating procedures, such as decompilation and goto-elimination. To demonstrate CF-GKAT\u2019s abilities, we validated the output of several highly non-trivial program transformations, such as Erosa and Hendren\u2019s\n                    <jats:monospace>goto<\/jats:monospace>\n                    -elimination procedure and the output of Ghidra decompiler. CF-GKAT opens up the application of Kleene Algebra to a wider set of challenges, and provides an important verification tool that can be applied to the field of decompilation and control-flow transformation.\n                  <\/jats:p>","DOI":"10.1145\/3704857","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"600-626","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["CF-GKAT: Efficient Validation of Control-Flow Transformations"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8197-6181","authenticated-orcid":false,"given":"Cheng","family":"Zhang","sequence":"first","affiliation":[{"name":"University College London, London, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6068-880X","authenticated-orcid":false,"given":"Tobias","family":"Kapp\u00e9","sequence":"additional","affiliation":[{"name":"Leiden University, Leiden, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3704-1060","authenticated-orcid":false,"given":"David E.","family":"Narv\u00e1ez","sequence":"additional","affiliation":[{"name":"Virginia Tech, Blacksburg, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3442-1543","authenticated-orcid":false,"given":"Nico","family":"Naus","sequence":"additional","affiliation":[{"name":"Open University of the Netherlands, Heerlen, Netherlands"},{"name":"Virginia Tech, Blacksburg, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2007.10.007"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","unstructured":"Carolyn Jane anderson Nate Foster Arjun Guha Jean-Baptiste Jeannin Dexter Kozen Cole Schlesinger and David Walker. 2014. NetKAT: semantic foundations for networks. In POPL. 113\u2013126. https:\/\/doi.org\/10.1145\/2535838.2535862 10.1145\/2535838.2535862","DOI":"10.1145\/2535838.2535862"},{"key":"e_1_3_2_4_2","volume-title":"Kleene Algebra with Tests and Program Schematology. Technical Report TR2001-1844","author":"Angus Allegra","year":"2001","unstructured":"Allegra Angus and Dexter Kozen. 2001. Kleene Algebra with Tests and Program Schematology. Technical Report TR2001-1844. Cornell University."},{"key":"e_1_3_2_5_2","unstructured":"Cheng Zhang Arthur Azevedo de Amorim and Marco Gaboardi. 2024. Kleene Algebra with Commutativity Conditions Is Undecidable. https:\/\/hal.science\/hal-04534715v2"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.COSE.2022.102608"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","unstructured":"Thomas Ball Rupak Majumdar Todd D. Millstein and Sriram K. Rajamani. 2001. Automatic Predicate Abstraction of C Programs. In PLDI. 203\u2013213. https:\/\/doi.org\/10.1145\/378795.378846 10.1145\/378795.378846","DOI":"10.1145\/378795.378846"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/355592.365646"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/321239.321249"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/3650212.3652144"},{"issue":"7","key":"e_1_3_2_11_2","first-page":"1009","article-title":"Une approche pour r\u00e9duire la complexit\u00e9 du flot de contr\u00f4le dans les programmes C","volume":"21","author":"Cass\u00e9 Hugues","year":"2002","unstructured":"Hugues Cass\u00e9, Louis F\u00e9raud, Christine Rochange, and Pascal Sainrat. 2002. Une approche pour r\u00e9duire la complexit\u00e9 du flot de contr\u00f4le dans les programmes C. Tech. Sci. Informatiques 21, 7 (2002), 1009\u20131032. http:\/\/tsi.revuesonline.com\/article.jsp?articleId=3831","journal-title":"Tech. Sci. Informatiques"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/3363562"},{"key":"e_1_3_2_13_2","volume-title":"Reverse compilation techniques","author":"Cifuentes Cristina","year":"1994","unstructured":"Cristina Cifuentes. 1994. Reverse compilation techniques. Ph. D. Dissertation. Queensland University of Technology."},{"key":"e_1_3_2_14_2","unstructured":"Ernie Cohen Dexter Kozen and Frederick Smith. 1996. The Complexity of Kleene Algebra with Tests. Technical Report TR96-1598."},{"key":"e_1_3_2_15_2","unstructured":"Coq Development Team. 2022. The Coq Reference Manual version 8.15. Available electronically at http:\/\/coq.inria.fr\/doc."},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","unstructured":"Sandeep Dasgupta Sushant Dinesh Deepan Venkatesh Vikram S. Adve and Christopher W. Fletcher. 2020. Scalable validation of binary lifters. In PLDI. 655\u2013671. https:\/\/doi.org\/10.1145\/3385412.3385964 10.1145\/3385412.3385964","DOI":"10.1145\/3385412.3385964"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICCL.1994.288377"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","unstructured":"Murdoch James Gabbay and Vincenzo Ciancia. 2011. Freshness and Name-Restriction in Sets of Traces with Names. In FoSSaCS. 365\u2013380. https:\/\/doi.org\/10.1007\/978-3-642-19805-2_25 10.1007\/978-3-642-19805-2_25","DOI":"10.1007\/978-3-642-19805-2_25"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","unstructured":"Benjamin Goldberg Lenore D. Zuck and Clark W. Barrett. 2004. Into the Loops: Practical Issues in Translation Validation for Optimizing Compilers. In COCV@ETAPS. 53\u201371. https:\/\/doi.org\/10.1016\/J.ENTCS.2005.01.030 10.1016\/J.ENTCS.2005.01.030","DOI":"10.1016\/J.ENTCS.2005.01.030"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603095"},{"key":"e_1_3_2_21_2","volume-title":"Translation validation for compilation verification","author":"Kasampalis Theodoros","year":"2021","unstructured":"Theodoros Kasampalis. 2021. Translation validation for compilation verification. Ph. D. Dissertation. University of Illinois Urbana-Champaign, USA. https:\/\/hdl.handle.net\/2142\/110460"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/3445814.3446751"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","unstructured":"Dexter Kozen. 1996. Kleene algebra with tests and commutativity conditions. In TACAS. 14\u201333. https:\/\/doi.org\/10.1007\/3-540-61042-1_35 10.1007\/3-540-61042-1_35","DOI":"10.1007\/3-540-61042-1_35"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","unstructured":"Dexter Kozen. 2008. Nonlocal Flow of Control and Kleene Algebra with Tests. In LICS. 105\u2013117. https:\/\/doi.org\/10.1109\/LICS.2008.32 10.1109\/LICS.2008.32","DOI":"10.1109\/LICS.2008.32"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","unstructured":"Dexter Kozen Konstantinos Mamouras Daniela Petrisan and Alexandra Silva. 2015. Nominal Kleene Coalgebra. In ICALP. 286\u2013298. https:\/\/doi.org\/10.1007\/978-3-662-47666-6_23 10.1007\/978-3-662-47666-6_23","DOI":"10.1007\/978-3-662-47666-6_23"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","unstructured":"Dexter Kozen Konstantinos Mamouras and Alexandra Silva. 2017. Completeness and incompleteness in nominal Kleene algebra. J. Log. Algebraic Methods Program. 91 17\u201332. https:\/\/doi.org\/10.1016\/J.JLAMP.2017.06.002 10.1016\/J.JLAMP.2017.06.002","DOI":"10.1016\/J.JLAMP.2017.06.002"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","unstructured":"Dexter Kozen and Maria-Christina Patron. 2000. Certification of Compiler Optimizations Using Kleene Algebra with Tests. In CL. 568\u2013582. https:\/\/doi.org\/10.1007\/3-540-44957-4_38 10.1007\/3-540-44957-4_38","DOI":"10.1007\/3-540-44957-4_38"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","unstructured":"Dexter Kozen and Frederick Smith. 1996. Kleene Algebra with Tests: Completeness and Decidability. In CSL. 244\u2013259. https:\/\/doi.org\/10.1007\/3-540-63172-0_43 10.1007\/3-540-63172-0_43","DOI":"10.1007\/3-540-63172-0_43"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","unstructured":"Dexter Kozen and Wei-Lung Dustin Tseng. 2008. The B\u00f6hm-Jacopini Theorem Is False Propositionally. In MPC. 177\u2013192. https:\/\/doi.org\/10.1007\/978-3-540-70594-9_11 10.1007\/978-3-540-70594-9_11","DOI":"10.1007\/978-3-540-70594-9_11"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","unstructured":"Stepan L. Kuznetsov. 2023. On the Complexity of Reasoning in Kleene Algebra with Commutativity Conditions. In ICTAC. 83\u201399. https:\/\/doi.org\/10.1007\/978-3-031-47963-2_7 10.1007\/978-3-031-47963-2_7","DOI":"10.1007\/978-3-031-47963-2_7"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","unstructured":"Vu Le Mehrdad Afshari and Zhendong Su. 2014. Compiler validation via equivalence modulo inputs. In PLDI. ACM 216\u2013226. https:\/\/doi.org\/10.1145\/2594291.2594334 10.1145\/2594291.2594334","DOI":"10.1145\/2594291.2594334"},{"key":"e_1_3_2_32_2","unstructured":"Xavier Leroy Sandrine Blazy Daniel K\u00e4stner Bernhard Schommer Markus Pister and Christian Ferdinand. 2016. CompCert \u2013 A Formally Verified Optimizing Compiler. In ERTS."},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","unstructured":"Zhibo Liu and Shuai Wang. 2020. How far we have come: testing decompilation correctness of C decompilers. In ISSTA. ACM 475\u2013487. https:\/\/doi.org\/10.1145\/3395363.3397370 10.1145\/3395363.3397370","DOI":"10.1145\/3395363.3397370"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","unstructured":"T.J. McCabe. 1976. A Complexity Measure. IEEE Transactions on Software Engineering SE-2 4 (1976) 308\u2013320. https:\/\/doi.org\/10.1109\/TSE.1976.233837 10.1109\/TSE.1976.233837","DOI":"10.1109\/TSE.1976.233837"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","unstructured":"Mark Moeller Jules Jacobs Olivier Savary B\u00e9langer David Darais Cole Schlesinger Steffen Smolka Nate Foster and Alexandra Silva. 2024. KATch: A Fast Symbolic Verifier for NetKAT. In PLDI. 1905\u20131928. https:\/\/doi.org\/10.1145\/3656454 10.1145\/3656454","DOI":"10.1145\/3656454"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","unstructured":"George C. Necula. 2000. Translation validation for an optimizing compiler. In PLDI. ACM 83\u201394. https:\/\/doi.org\/10.1145\/349299.349314 10.1145\/349299.349314","DOI":"10.1145\/349299.349314"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","unstructured":"Georg Neis Chung-Kil Hur Jan-Oliver Kaiser Craig McLaughlin Derek Dreyer and Viktor Vafeiadis. 2015. Pilsner: a compositionally verified compiler for a higher-order imperative language. In ICFP. ACM 166\u2013178. https:\/\/doi.org\/10.1145\/2784731.2784764 10.1145\/2784731.2784764","DOI":"10.1145\/2784731.2784764"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","unstructured":"Amir Pnueli Michael Siegel and Eli Singerman. 1998. Translation Validation. In TACAS. 151\u2013166. https:\/\/doi.org\/10.1007\/BFB0054170 10.1007\/BFB0054170","DOI":"10.1007\/BFB0054170"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","unstructured":"Damien Pous. 2015. Symbolic Algorithms for Language Equivalence and Kleene Algebra with Tests. In POPL. 357\u2013368. https:\/\/doi.org\/10.1145\/2676726.2677007 10.1145\/2676726.2677007","DOI":"10.1145\/2676726.2677007"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","unstructured":"Todd Schmid Tobias Kapp\u00e9 Dexter Kozen and Alexandra Silva. 2021. Guarded Kleene Algebra with Tests: Coequations Coinduction and Completeness. 142:1-142:14 pages. https:\/\/doi.org\/10.4230\/LIPICS.ICALP.2021.142 10.4230\/LIPICS.ICALP.2021.142","DOI":"10.4230\/LIPICS.ICALP.2021.142"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","unstructured":"Thomas Arthur Leck Sewell Magnus O. Myreen and Gerwin Klein. 2013. Translation validation for a verified OS kernel. In PLDI. ACM 471\u2013482. https:\/\/doi.org\/10.1145\/2491956.2462183 10.1145\/2491956.2462183","DOI":"10.1145\/2491956.2462183"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","unstructured":"Steffen Smolka Nate Foster Justin Hsu Tobias Kapp\u00e9 Dexter Kozen and Alexandra Silva. 2020. Guarded Kleene algebra with tests: verification of uninterpreted programs in nearly linear time. In POPL. 61:1\u201361:28. https:\/\/doi.org\/10.1145\/3371129 10.1145\/3371129","DOI":"10.1145\/3371129"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","unstructured":"Yong Kiam Tan Magnus O. Myreen Ramana Kumar Anthony C. J. Fox Scott Owens and Michael Norrish. 2016. A new verified compiler backend for CakeML. In ICFP. ACM 60\u201373. https:\/\/doi.org\/10.1145\/2951913.2951924 10.1145\/2951913.2951924","DOI":"10.1145\/2951913.2951924"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","unstructured":"Robert Endre Tarjan. 1975. Efficiency of a Good But Not Linear Set Union Algorithm. J. ACM 22 2 (1975) 215\u2013225. https:\/\/doi.org\/10.1145\/321879.321884 10.1145\/321879.321884","DOI":"10.1145\/321879.321884"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","unstructured":"Balder ten Cate and Tobias Kapp\u00e9. 2025. Algebras for Deterministic Computation are Inherently Incomplete. In POPL. 25:1\u201325:27. https:\/\/doi.org\/10.1145\/3704861 10.1145\/3704861","DOI":"10.1145\/3704861"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","unstructured":"Ken Thompson. 1968. Regular Expression Search Algorithm. Commun. ACM 11 6 (1968) 419\u2013422. https:\/\/doi.org\/10.1145\/363347.363387 10.1145\/363347.363387","DOI":"10.1145\/363347.363387"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","unstructured":"Freek Verbeek Joshua A. Bockenek Zhoulai Fu and Binoy Ravindran. 2022. Formally verified lifting of C-compiled x86-64 binaries. In PLDI. ACM 934\u2013949. https:\/\/doi.org\/10.1145\/3519939.3523702 10.1145\/3519939.3523702","DOI":"10.1145\/3519939.3523702"},{"key":"e_1_3_2_48_2","doi-asserted-by":"crossref","unstructured":"Freek Verbeek Nico Naus and Binoy Ravindran. 2024. Verifiably Correct Lifting of Position-Independent x86-64 Binaries to Symbolized Assembly. In CCS.","DOI":"10.1145\/3658644.3690244"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","unstructured":"Freek Verbeek Pierre Olivier and Binoy Ravindran. 2020. Sound C Code Decompilation for a Subset of x86-64 Binaries. In SEFM. 247\u2013264. https:\/\/doi.org\/10.1007\/978-3-030-58768-0_14 10.1007\/978-3-030-58768-0_14","DOI":"10.1007\/978-3-030-58768-0_14"},{"key":"e_1_3_2_50_2","doi-asserted-by":"crossref","unstructured":"Khaled Yakdan Sebastian Eschweiler Elmar Gerhards-Padilla and Matthew Smith. 2015. No More Gotos: De compilation Using Pattern-Independent Control-Flow Structuring and Semantic-Preserving Transformations. In NDSS. https:\/\/www.ndss-symposium.org\/ndss2015\/no-more-gotos-decompilation-using-pattern-independent-control-flow-structuring-and-semantics","DOI":"10.14722\/ndss.2015.23185"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","unstructured":"Xuejun Yang Yang Chen Eric Eide and John Regehr. 2011. Finding and understanding bugs in C compilers. In PLDI. ACM 283\u2013294. https:\/\/doi.org\/10.1145\/1993498.1993532 10.1145\/1993498.1993532","DOI":"10.1145\/1993498.1993532"},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","unstructured":"Cheng Zhang Tobias Kapp\u00e9 David E. Narva\u00e9z and Nico Naus. 2024. CF-GKAT: Efficient Validation of Control-Flow Transformations (Artifact). https:\/\/doi.org\/10.5281\/zenodo.13938565 10.5281\/zenodo.13938565","DOI":"10.5281\/zenodo.13938565"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","unstructured":"Yiji Zhang and Lenore D. Zuck. 2018. Formal Verification of Optimizing Compilers. In ICDCIT. 50\u201365. https:\/\/doi.org\/10.1007\/978-3-319-72344-0_3 10.1007\/978-3-319-72344-0_3","DOI":"10.1007\/978-3-319-72344-0_3"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704857","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704857","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:16:28Z","timestamp":1770200188000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704857"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":52,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704857"],"URL":"https:\/\/doi.org\/10.1145\/3704857","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"}}]}}