{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,6]],"date-time":"2025-12-06T17:19:00Z","timestamp":1765041540451,"version":"3.41.0"},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2024,4,29]],"date-time":"2024-04-29T00:00:00Z","timestamp":1714348800000},"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":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,4,29]]},"abstract":"<jats:p>Parameterized verification is a challenging problem that is known to be undecidable in the general case. \u2004\u200dis a widely-used method for parameterized verification, originally proposed by Chou, Mannava and Park in 2004. It involves abstracting the protocol to a small fixed number of nodes, and strengthening by auxiliary invariants to refine the abstraction. In most of the existing applications of CMP, the abstraction and strengthening procedures are carried out manually, which can be tedious and error-prone. Existing theoretical justification of the \u2004\u200dmethod is also done at a high level, without detailed descriptions of abstraction and strengthening rules. In this paper, we present a formally verified theory of \u2004\u200din Isabelle\/HOL, with detailed, syntax-directed procedure for abstraction and strengthening that is proven correct. The formalization also includes correctness of symmetry reduction and assume-guarantee reasoning. We also describe a tool AutoCMP for automatically carrying out abstraction and strengthening in , as well as generating Isabelle proof scripts showing their correctness. We applied the tool to a number of parameterized protocols, and discovered some inaccuracies in previous manual applications of \u2004\u200dto the FLASH cache coherence protocol.<\/jats:p>","DOI":"10.1145\/3649858","type":"journal-article","created":{"date-parts":[[2024,4,29]],"date-time":"2024-04-29T17:53:50Z","timestamp":1714413230000},"page":"1324-1350","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Mechanizing the CMP Abstraction for Parameterized Verification"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2817-063X","authenticated-orcid":false,"given":"Yongjian","family":"Li","sequence":"first","affiliation":[{"name":"Institute of Software at Chinese Academy of Sciences, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5377-9351","authenticated-orcid":false,"given":"Bohua","family":"Zhan","sequence":"additional","affiliation":[{"name":"Institute of Software at Chinese Academy of Sciences, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4521-4112","authenticated-orcid":false,"given":"Jun","family":"Pang","sequence":"additional","affiliation":[{"name":"University of Luxembourg, Luxembourg, Luxembourg"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,4,29]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"crossref","unstructured":"Parosh Aziz Abdulla A. Prasad Sistla and Muralidhar Talupur. 2018. Model Checking Parameterized Systems. In Handbook of Model Checking. 685\u2013725.","DOI":"10.1007\/978-3-319-10575-8_21"},{"key":"e_1_2_1_2_1","doi-asserted-by":"crossref","first-page":"307","DOI":"10.1016\/0020-0190(86)90071-2","article-title":"Limits for Automatic Verification of Finite-State Concurrent Systems","volume":"22","author":"Apt Krzysztof R.","year":"1986","unstructured":"Krzysztof R. Apt and Dexter Kozen. 1986. Limits for Automatic Verification of Finite-State Concurrent Systems. Inform. Process. Lett., 22, 6 (1986), 307\u2013309.","journal-title":"Inform. Process. Lett."},{"key":"e_1_2_1_3_1","volume-title":"Proc. 13th International Conference on Computer Aided Verification (CAV\u201901)","volume":"234","author":"Arons Tamarah","unstructured":"Tamarah Arons, Amir Pnueli, Sitvanit Ruah, Jiazhao Xu, and Lenore D. Zuck. 2001. Parameterized Verification with Automatically Computed Inductive Assertions. In Proc. 13th International Conference on Computer Aided Verification (CAV\u201901) (Lecture Notes in Computer Science, Vol. 2102). Springer, 221\u2013234."},{"key":"e_1_2_1_4_1","volume-title":"Proc. 33rd IEEE\/ACM International Conference on Automated Software Engineering (ASE\u201918)","author":"Cao Jialun","year":"2018","unstructured":"Jialun Cao, Yongjian Li, and Jun Pang. 2018. L-CMP: An automatic learning-based parameterized verification tool (Tool Demo). In Proc. 33rd IEEE\/ACM International Conference on Automated Software Engineering (ASE\u201918). ACM Press, 892\u2013895."},{"volume-title":"Proc. 37th IEEE International Conference on Computer Design (ICCD\u201919)","author":"Cao J.","key":"e_1_2_1_5_1","unstructured":"J. Cao, Y. Li, and J. Pang. 2019. A learning-based framework for automatic parameterized verification. In Proc. 37th IEEE International Conference on Computer Design (ICCD\u201919). IEEE CS, 450\u2013459."},{"key":"e_1_2_1_7_1","volume-title":"Proc. 6th International Conference on Formal Methods in Computer Aided Design (FMCAD\u201906)","author":"Chen Xiaofang","year":"2006","unstructured":"Xiaofang Chen, Yu Yang, Ganesh Gopalakrishnan, and Ching-Tsun Chou. 2006. Reducing Verification Complexity of a Multicore Coherence Protocol using Assume\/guarantee. In Proc. 6th International Conference on Formal Methods in Computer Aided Design (FMCAD\u201906). IEEE Computer Society, 81\u201388."},{"key":"e_1_2_1_8_1","volume-title":"Proc. 5th International Conference on Formal Methods in Computer-Aided Design (FMCAD\u201904)","volume":"398","author":"Chou Ching-Tsun","year":"2004","unstructured":"Ching-Tsun Chou, Phanindra K. Mannava, and Seungjoon Park. 2004. A Simple Method for Parameterized Verification of Cache Coherence Protocols. In Proc. 5th International Conference on Formal Methods in Computer-Aided Design (FMCAD\u201904) (Lecture Notes in Computer Science, Vol. 3312). Springer, 382\u2013398."},{"key":"e_1_2_1_9_1","doi-asserted-by":"crossref","first-page":"752","DOI":"10.1145\/876638.876643","article-title":"Counterexample-Guided Abstraction Refinement for Symbolic Model Checking","volume":"50","author":"Clarke Edmund","year":"2003","unstructured":"Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. 2003. Counterexample-Guided Abstraction Refinement for Symbolic Model Checking. J. ACM, 50, 5 (2003), 752\u2013794. issn:0004-5411","journal-title":"J. ACM"},{"volume-title":"Handbook of Model Checking","author":"Clarke Edmund M.","key":"e_1_2_1_10_1","unstructured":"Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem. 2018. Handbook of Model Checking. Springer."},{"key":"e_1_2_1_11_1","doi-asserted-by":"crossref","first-page":"104","DOI":"10.1007\/s10703-008-0063-8","article-title":"Local Proofs for Global Safety Properties","volume":"34","author":"Cohen Ariel","year":"2009","unstructured":"Ariel Cohen and Kedar S. Namjoshi. 2009. Local Proofs for Global Safety Properties. Formal Methods in System Design, 34, 2 (2009), 104\u2013125.","journal-title":"Formal Methods in System Design"},{"key":"e_1_2_1_12_1","volume-title":"Proc. 9th International Joint Conference on Automated Reasoning (IJCAR\u201918)","volume":"160","author":"Conchon Sylvain","year":"2018","unstructured":"Sylvain Conchon, David Declerck, and Fatiha Za\u00efdi. 2018. Cubicle-W: Parameterized Model Checking on Weak Memory. In Proc. 9th International Joint Conference on Automated Reasoning (IJCAR\u201918) (Lecture Notes in Computer Science, Vol. 10900). 152\u2013160."},{"key":"e_1_2_1_13_1","volume-title":"Proc. 24th International Conference on Computer Aided Verification (CAV\u201912)","volume":"724","author":"Conchon Sylvain","year":"2012","unstructured":"Sylvain Conchon, Amit Goel, Sava Krstic, Alain Mebsout, and Fatiha Za\u00efdi. 2012. Cubicle: A Parallel SMT-Based Model Checker for Parameterized Systems - Tool Paper. In Proc. 24th International Conference on Computer Aided Verification (CAV\u201912) (Lecture Notes in Computer Science, Vol. 7358). Springer, 718\u2013724."},{"key":"e_1_2_1_14_1","volume-title":"Proc. 13th International Conference on Formal Methods in Computer-Aided Design (FMCAD\u201913)","author":"Conchon Sylvain","year":"2013","unstructured":"Sylvain Conchon, Amit Goel, Sava Krstic, Alain Mebsout, and Fatiha Za\u00efdi. 2013. Invariants for Finite Instances and Beyond. In Proc. 13th International Conference on Formal Methods in Computer-Aided Design (FMCAD\u201913). IEEE Computer Society, 61\u201368."},{"key":"e_1_2_1_15_1","volume-title":"Proc. 8th International Conference on Computer Aided Verification (CAV\u201996)","volume":"393","author":"Dill David L.","year":"1996","unstructured":"David L. Dill. 1996. The Murphi Verification System. In Proc. 8th International Conference on Computer Aided Verification (CAV\u201996) (Lecture Notes in Computer Science, Vol. 1102). Springer, 390\u2013393."},{"key":"e_1_2_1_16_1","volume-title":"Proc. 31th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI\u201910)","author":"Emmi Michael","year":"2010","unstructured":"Michael Emmi, Rupak Majumdar, and Roman Manevich. 2010. Parameterized Verification of Transactional Memories. In Proc. 31th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI\u201910). ACM Press, 134\u2013145."},{"key":"e_1_2_1_17_1","volume-title":"Proc. 25th International Conference on Computer Aided Verification (CAV\u201913)","volume":"478","author":"Esparza Javier","year":"2013","unstructured":"Javier Esparza, Peter Lammich, Ren\u00e9 Neumann, Tobias Nipkow, Alexander Schimpf, and Jan-Georg Smaus. 2013. A Fully Verified Executable LTL Model Checker. In Proc. 25th International Conference on Computer Aided Verification (CAV\u201913) (Lecture Notes in Computer Science, Vol. 8044). Springer, 463\u2013478."},{"key":"e_1_2_1_18_1","volume-title":"Proc. 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL\u201917)","author":"Hoenicke Jochen","year":"2017","unstructured":"Jochen Hoenicke, Rupak Majumdar, and Andreas Podelski. 2017. Thread Modularity at Many Levels: A Pearl in Compositional Verification. In Proc. 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL\u201917). ACM Press, 473\u2013485."},{"key":"e_1_2_1_19_1","volume-title":"Proc. 6th European Workshop on Applications and Theory in Petri Nets (Lecture Notes in Computer Science","volume":"233","author":"Huber Peter","year":"1984","unstructured":"Peter Huber, Arne M. Jensen, Leif O. Jepsen, and Kurt Jensen. 1984. Towards Reachability Trees for High-level Petri Nets. In Proc. 6th European Workshop on Applications and Theory in Petri Nets (Lecture Notes in Computer Science, Vol. 188). Springer, 215\u2013233."},{"volume-title":"Proc. International Conference on Computer Design (ICCD\u201993)","author":"Norris Ip C.","key":"e_1_2_1_20_1","unstructured":"C. Norris Ip and David L. Dill. 1993. Efficient Verification of Symmetric Concurrent Systems. In Proc. International Conference on Computer Design (ICCD\u201993). IEEE Computer Soceity, 230\u2013234."},{"key":"e_1_2_1_21_1","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1007\/BF00625968","article-title":"Better Verification through Symmetry","volume":"9","author":"Norris Ip C.","year":"1996","unstructured":"C. Norris Ip and David L. Dill. 1996. Better Verification through Symmetry. Formal Methods in System Design, 9, 1\/2 (1996), 41\u201375.","journal-title":"Formal Methods in System Design"},{"key":"e_1_2_1_22_1","volume-title":"Proc. 4th Workshop on Automated Verification of Infinite State Systems (AVIS\u201905)","author":"Krstic Sava","year":"2005","unstructured":"Sava Krstic. 2005. Parameterized System Verification with Guard Strengthening and Parameter Abstraction. Proc. 4th Workshop on Automated Verification of Infinite State Systems (AVIS\u201905)."},{"key":"e_1_2_1_23_1","volume-title":"Proc. 5th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI\u201904)","volume":"281","author":"Shuvendu","unstructured":"Shuvendu K. Lahiri and Randal E. Bryant. 2004. Constructing Quantified Invariants via Predicate Abstraction. In Proc. 5th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI\u201904) (Lecture Notes in Computer Science, Vol. 2937). Springer, 267\u2013281."},{"key":"e_1_2_1_24_1","volume-title":"Proc. 34th IEEE International Conference on Computer Design (ICCD\u201916)","author":"Li Yongjian","year":"2016","unstructured":"Yongjian Li, Kaiqiang Duan, Yi Lv, Jun Pang, and Shaowei Cai. 2016. A Novel Approach to Parameterized Verification of Cache Coherence Protocols. In Proc. 34th IEEE International Conference on Computer Design (ICCD\u201916). IEEE Computer Society, 560\u2013567."},{"key":"e_1_2_1_25_1","unstructured":"Yongjian Li and Zimin Li. 2022. ILCMP source code. https:\/\/gitee.com\/dust_capacity_i\/ILCMP.git"},{"key":"e_1_2_1_26_1","unstructured":"Yongjian Li Zimin Li Bohua Zhan and Jun Pang. 2023. autoCMP. https:\/\/github.com\/forSubmission238\/autoCMP"},{"key":"e_1_2_1_27_1","volume-title":"Proc. 10th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME\u201999)","volume":"234","author":"McMillan Kenneth L.","year":"1999","unstructured":"Kenneth L. McMillan. 1999. Verification of Infinite State Systems by Compositional Model Checking. In Proc. 10th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME\u201999) (Lecture Notes in Computer Science, Vol. 1703). Springer, 219\u2013234."},{"key":"e_1_2_1_28_1","volume-title":"Proc. 11th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME\u201901)","volume":"195","author":"McMillan Kenneth L.","year":"2001","unstructured":"Kenneth L. McMillan. 2001. Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking. In Proc. 11th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME\u201901) (Lecture Notes in Computer Science, Vol. 2144). Springer, 179\u2013195."},{"key":"e_1_2_1_29_1","volume-title":"Proc. 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201908)","volume":"427","author":"McMillan Kenneth L.","year":"2008","unstructured":"Kenneth L. McMillan. 2008. Quantified Invariant Generation using An Interpolating Saturation Prover. In Proc. 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201908) (Lecture Notes in Computer Science, Vol. 4963). Springer, 413\u2013427."},{"key":"e_1_2_1_30_1","volume-title":"Proc. 16th International Conference on Formal Methods in Computer-Aided Design (FMCAD\u201916)","author":"McMillan Kenneth L.","year":"2016","unstructured":"Kenneth L. McMillan. 2016. Modular Specification and Verification of a Cache-coherent Interface. In Proc. 16th International Conference on Formal Methods in Computer-Aided Design (FMCAD\u201916). IEEE, 109\u2013116."},{"key":"e_1_2_1_31_1","volume-title":"Proc. 30th International Conference on Computer Aided Verification (CAV\u201918)","volume":"208","author":"McMillan Kenneth L.","year":"2018","unstructured":"Kenneth L. McMillan. 2018. Eager Abstraction for Symbolic Model Checking. In Proc. 30th International Conference on Computer Aided Verification (CAV\u201918) (Lecture Notes in Computer Science, Vol. 10981). Springer, 191\u2013208."},{"key":"e_1_2_1_32_1","doi-asserted-by":"crossref","unstructured":"Tobias Nipkow Lawrence C. Paulson and Markus Wenzel. 2002. Isabelle\/HOL - A Proof Assistant for Higher-Order Logic (Lecture Notes in Computer Science Vol. 2283). Springer.","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_2_1_33_1","volume-title":"Proc. 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI\u201918)","author":"Padon Oded","year":"2016","unstructured":"Oded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv, and Sharon Shoham. 2016. Ivy: Safety Verification by Interactive Generalization. In Proc. 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI\u201918). ACM Press, 614\u2013630."},{"key":"e_1_2_1_34_1","volume-title":"Proc. 13th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME\u201905)","volume":"331","author":"Pandav Sudhindra","year":"2005","unstructured":"Sudhindra Pandav, Konrad Slind, and Ganesh Gopalakrishnan. 2005. Counterexample Guided Invariant Discovery for Parameterized Cache Coherence Verification. In Proc. 13th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME\u201905) (Lecture Notes in Computer Science, Vol. 3725). Springer, 317\u2013331."},{"key":"e_1_2_1_35_1","volume-title":"Proc. 8th ACM Symposium on Parallel Algorithms and Architectures (SPAA\u201996)","author":"Park Seungjoon","year":"1996","unstructured":"Seungjoon Park and David L Dill. 1996. Verification of FLASH Cache Coherence Protocol by Aggregation of Distributed Transactions. In Proc. 8th ACM Symposium on Parallel Algorithms and Architectures (SPAA\u201996). ACM, 288\u2013296."},{"key":"e_1_2_1_36_1","volume-title":"Proc. 7th International Conference Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201901)","volume":"97","author":"Pnueli Amir","unstructured":"Amir Pnueli, Sitvanit Ruah, and Lenore D. Zuck. 2001. Automatic Deductive Verification with Invisible Invariants. In Proc. 7th International Conference Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201901) (Lecture Notes in Computer Science, Vol. 2031). Springer, 82\u201397."},{"key":"e_1_2_1_37_1","volume-title":"Proc. 8th International Conference on Computer Aided Verification (CAV\u201996)","volume":"195","author":"Pnueli Amir","year":"1996","unstructured":"Amir Pnueli and Elad Shahar. 1996. A Platform for Combining Deductive with Algorithmic Verification. In Proc. 8th International Conference on Computer Aided Verification (CAV\u201996) (Lecture Notes in Computer Science, Vol. 1102). Springer, 184\u2013195."},{"key":"e_1_2_1_38_1","first-page":"4","article-title":"Reachability analysis of Petri Nets using Symmetries","volume":"8","author":"Starke Peter H","year":"1991","unstructured":"Peter H Starke. 1991. Reachability analysis of Petri Nets using Symmetries. Systems Analysis Modelling Simulation, 8, 4-5 (1991), 293\u2013303.","journal-title":"Systems Analysis Modelling Simulation"},{"volume-title":"Proc. 8th International Conference on Formal Methods in Computer-Aided Design (FMCAD\u201908)","author":"Talupur Murali","key":"e_1_2_1_39_1","unstructured":"Murali Talupur and Mark R. Tuttle. 2008. Going with the Flow: Parameterized Verification using Message Flows. In Proc. 8th International Conference on Formal Methods in Computer-Aided Design (FMCAD\u201908). IEEE Computer Society, 1\u20138."},{"key":"e_1_2_1_40_1","volume-title":"Proc. 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI\u201918)","author":"Taube Marcelo","year":"2018","unstructured":"Marcelo Taube, Giuliano Losa, Kenneth L. McMillan, Oded Padon, Mooly Sagiv, Sharon Shoham, James R. Wilcox, and Doug Woos. 2018. Modularity for Decidability of Deductive Verification with Applications to Distributed Systems. In Proc. 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI\u201918). ACM Press, 662\u2013677."},{"key":"e_1_2_1_41_1","volume-title":"Proc. 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201901)","volume":"127","author":"Tiwari Ashish","year":"2001","unstructured":"Ashish Tiwari, Harald Rue\u00df, Hassen Sa\u00efdi, and Natarajan Shankar. 2001. A Technique for Invariant Generation. In Proc. 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201901) (Lecture Notes in Computer Science, Vol. 2031). Springer, 113\u2013127."},{"key":"e_1_2_1_42_1","volume-title":"Proc. 13th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL\u201986)","author":"Wolper Pierre","year":"1986","unstructured":"Pierre Wolper. 1986. Expressing Interesting Properties of Programs in Propositional Temporal Logic. In Proc. 13th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL\u201986). ACM Press, 184\u2013193."},{"key":"e_1_2_1_43_1","volume-title":"Proc. 1st International Conference on Computer Aided Verification (CAV\u201989)","volume":"80","author":"Wolper Pierre","year":"1989","unstructured":"Pierre Wolper and Vinciane Lovinfosse. 1989. Verifying Properties of Large Sets of Processes with Network Invariants. In Proc. 1st International Conference on Computer Aided Verification (CAV\u201989) (Lecture Notes in Computer Science, Vol. 407). Springer, 60\u201380."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3649858","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3649858","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:54:07Z","timestamp":1750287247000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3649858"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,29]]},"references-count":42,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2024,4,29]]}},"alternative-id":["10.1145\/3649858"],"URL":"https:\/\/doi.org\/10.1145\/3649858","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2024,4,29]]},"assertion":[{"value":"2024-04-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}