{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T06:58:54Z","timestamp":1779087534271,"version":"3.51.4"},"reference-count":89,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T00:00:00Z","timestamp":1667174400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"The National Natural Science Foundation of China","award":["62172271"],"award-info":[{"award-number":["62172271"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,10,31]]},"abstract":"<jats:p>\n            Invariant generation is a classical problem to automatically generate invariants to aid the formal analysis of programs. In this work, we consider the problem of generating tight linear-invariants over affine programs (i.e., programs with affine guards and updates) without a prescribed goal property. In the literature, the only known sound and complete characterization to solve this problem is via Farkas\u2019 Lemma (FL), and has been implemented through either quantifier elimination or reasonable heuristics. Although FL-based approaches can generate highly accurate linear invariants from the completeness of FL, the main bottleneck to applying these approaches is the scalability issue caused by either non-linear constraints or combinatorial explosion. We base our approach on the only practical FL-based approach [Sankaranarayanan\u2004\u200d\n            <jats:italic>et al.<\/jats:italic>\n            , SAS 2004] that applies FL with reasonable heuristics, and develop two novel and independent improvements to leverage the scalability. The first improvement is the novel idea to generate invariants at one program location in a single invariant-generation process, so that the invariants for each location are generated separately rather than together in a single computation. This idea naturally leads to a parallel processing that divides the invariant-generation task for all program locations by assigning the locations separately to multiple processors. Moreover, the idea enables us to develop detailed technical improvements to further reduce the combinatorial explosion in the original work [Sankaranarayanan\u2004\u200d\n            <jats:italic>et al.<\/jats:italic>\n            , SAS 2004]. The second improvement is a segmented subsumption testing in the CNF-to-DNF expansion that allows discovering more local subsumptions in advance. We formally prove that our approach has the same accuracy as the original work and thus does not incur accuracy loss on the generated invariants. Moreover, experimental results on representative benchmarks involving non-trivial linear invariants demonstrate that our approach improves the runtime of the original work by several orders of magnitude, even in the non-parallel scenario that sums up the execution time for all program locations. Hence, our approach constitutes the first significant improvement in FL-based approaches for linear invariant generation after almost two decades.\n          <\/jats:p>","DOI":"10.1145\/3563295","type":"journal-article","created":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T20:23:35Z","timestamp":1667247815000},"page":"204-232","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["Scalable linear invariant generation with Farkas\u2019 lemma"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8987-596X","authenticated-orcid":false,"given":"Hongming","family":"Liu","sequence":"first","affiliation":[{"name":"Shanghai Jiao Tong University, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7947-3446","authenticated-orcid":false,"given":"Hongfei","family":"Fu","sequence":"additional","affiliation":[{"name":"Shanghai Jiao Tong University, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9756-9540","authenticated-orcid":false,"given":"Zhiyong","family":"Yu","sequence":"additional","affiliation":[{"name":"Shanghai Jiao Tong University, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4847-9183","authenticated-orcid":false,"given":"Jiaxin","family":"Song","sequence":"additional","affiliation":[{"name":"Shanghai Jiao Tong University, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9005-7112","authenticated-orcid":false,"given":"Guoqiang","family":"Li","sequence":"additional","affiliation":[{"name":"Shanghai Jiao Tong University, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,10,31]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48288-9_14"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(1:1)2012"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_48"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15769-1_8"},{"key":"e_1_2_1_5_1","unstructured":"2021. Arduino: An open-source electronics platform based on easy-to-use hardware and software. https:\/\/github.com\/arkhipenko\/TaskScheduler \t\t\t\t  2021. Arduino: An open-source electronics platform based on easy-to-use hardware and software. https:\/\/github.com\/arkhipenko\/TaskScheduler"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1137\/0213054"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454076"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44898-5_19"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45789-5_17"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_4"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_48"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386035"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1277548.1277557"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10936-7_6"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3339984"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385969"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009873"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_44"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-75292-9_3"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_39"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45319-9_6"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_1"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31987-0_3"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512770"},{"key":"e_1_2_1_26_1","unstructured":"2022. CPAchecker: The Configurable Software-Verification Platform. https:\/\/cpachecker.sosy-lab.org \t\t\t\t  2022. CPAchecker: The Configurable Software-Verification Platform. https:\/\/cpachecker.sosy-lab.org"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1368088.1368127"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(88)80004-X"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48989-6_12"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-46520-3_30"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-68167-2_22"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509511"},{"key":"e_1_2_1_33_1","volume-title":"A Fourier-f\u00e9le mechanikai elv alkalmaz\u00e1sai (Hungarian). Mathematikai\u00e9s Term\u00e9szettudom\u00e1nyi \u00c9rtesit\u00f6, 12","author":"Farkas J.","year":"1894","unstructured":"J. Farkas . 1894. A Fourier-f\u00e9le mechanikai elv alkalmaz\u00e1sai (Hungarian). Mathematikai\u00e9s Term\u00e9szettudom\u00e1nyi \u00c9rtesit\u00f6, 12 ( 1894 ), 457\u2013472. J. Farkas. 1894. A Fourier-f\u00e9le mechanikai elv alkalmaz\u00e1sai (Hungarian). Mathematikai\u00e9s Term\u00e9szettudom\u00e1nyi \u00c9rtesit\u00f6, 12 (1894), 457\u2013472."},{"key":"e_1_2_1_34_1","volume-title":"Compositional Recurrence Analysis","author":"Farzan Azadeh","unstructured":"Azadeh Farzan and Zachary Kincaid . 2015. Compositional Recurrence Analysis . In FMCAD. IEEE , 57\u201364. Azadeh Farzan and Zachary Kincaid. 2015. Compositional Recurrence Analysis. In FMCAD. IEEE, 57\u201364."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2018.8603011"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_14"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-68167-2_26"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53288-8_20"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_5"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837664"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0000474"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375616"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-93900-9_13"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_48"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008678014487"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386016"},{"key":"e_1_2_1_47_1","volume-title":"Model checking strategies for linear hybrid systems","author":"Henzinger Thomas A","unstructured":"Thomas A Henzinger and Pei-Hsin Ho. 1994. Model checking strategies for linear hybrid systems . Cornell University . Thomas A Henzinger and Pei-Hsin Ho. 1994. Model checking strategies for linear hybrid systems. Cornell University."},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33125-1_6"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209142"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3087604.3087623"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-67067-2_2"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13185-1_13"},{"key":"e_1_2_1_53_1","volume-title":"Automatically Generating Loop Invariants Using Quantifier Elimination. In Deduction and Applications (Dagstuhl Seminar Proceedings","volume":"511","author":"Kapur Deepak","year":"2005","unstructured":"Deepak Kapur . 2005 . Automatically Generating Loop Invariants Using Quantifier Elimination. In Deduction and Applications (Dagstuhl Seminar Proceedings , Vol. 05431). Internationales Begegnungs- und Forschungszentrum f\u00fcr Informatik (IBFI), Schloss Dagstuhl, Germany. http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2006\/ 511 Deepak Kapur. 2005. Automatically Generating Loop Invariants Using Quantifier Elimination. In Deduction and Applications (Dagstuhl Seminar Proceedings, Vol. 05431). Internationales Begegnungs- und Forschungszentrum f\u00fcr Informatik (IBFI), Schloss Dagstuhl, Germany. http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2006\/511"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15769-1_24"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062373"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158142"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/7351.7352"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11704-014-3150-6"},{"key":"e_1_2_1_59_1","unstructured":"Hongming Liu Hongfei Fu Zhiyong Yu Jiaxin Song and Guoqiang Li. 2022. Scalable Linear Invariant Generation with Farkas\u2019 Lemma. March https:\/\/hal.archives-ouvertes.fr\/hal-03463338 working paper or preprint \t\t\t\t  Hongming Liu Hongfei Fu Zhiyong Yu Jiaxin Song and Guoqiang Li. 2022. Scalable Linear Invariant Generation with Farkas\u2019 Lemma. March https:\/\/hal.archives-ouvertes.fr\/hal-03463338 working paper or preprint"},{"key":"e_1_2_1_60_1","volume-title":"Temporal verification of reactive systems - safety","author":"Manna Zohar","unstructured":"Zohar Manna and Amir Pnueli . 1995. Temporal verification of reactive systems - safety . Springer . isbn:978-0-387-94459-3 Zohar Manna and Amir Pnueli. 1995. Temporal verification of reactive systems - safety. Springer. isbn:978-0-387-94459-3"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_31"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2004.05.004"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2012.6227149"},{"key":"e_1_2_1_64_1","unstructured":"2022. OCRS: Operational calculus recurrence solver. https:\/\/github.com\/cyphertjohn\/OCRS \t\t\t\t  2022. OCRS: Operational calculus recurrence solver. https:\/\/github.com\/cyphertjohn\/OCRS"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908099"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908118"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_20"},{"key":"e_1_2_1_68_1","unstructured":"2021. Parma Polyhedra Library PPL 1.2. https:\/\/www.bugseng.com\/parma-polyhedra-library. \t\t\t\t  2021. Parma Polyhedra Library PPL 1.2. https:\/\/www.bugseng.com\/parma-polyhedra-library."},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27864-1_21"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/1005285.1005324"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2006.03.003"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964028"},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27864-1_7"},{"key":"e_1_2_1_74_1","volume-title":"Theory of linear and integer programming","author":"Schrijver Alexander","unstructured":"Alexander Schrijver . 1999. Theory of linear and integer programming . Wiley . isbn:978-0-471-98232-6 Alexander Schrijver. 1999. Theory of linear and integer programming. Wiley. isbn:978-0-471-98232-6"},{"key":"e_1_2_1_75_1","unstructured":"2015. SeaHorn: A fully automated analysis framework for LLVM-based languages. http:\/\/seahorn.github.io \t\t\t\t  2015. SeaHorn: A fully automated analysis framework for LLVM-based languages. http:\/\/seahorn.github.io"},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0248-5"},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_57"},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_31"},{"key":"e_1_2_1_79_1","volume-title":"Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017","author":"Singh Gagandeep","year":"2017","unstructured":"Gagandeep Singh , Markus P\u00fcschel , and Martin T. Vechev . 2017. Fast polyhedra abstract domain . In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017 , Paris, France , January 18-20, 2017 , Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 46\u201359. Gagandeep Singh, Markus P\u00fcschel, and Martin T. Vechev. 2017. Fast polyhedra abstract domain. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 46\u201359."},{"key":"e_1_2_1_80_1","unstructured":"2021. Sparse: C language semantic parser. https:\/\/lwn.net\/Articles\/689907\/ \t\t\t\t  2021. Sparse: C language semantic parser. https:\/\/lwn.net\/Articles\/689907\/"},{"key":"e_1_2_1_81_1","unstructured":"2006. StInG: Stanford Invariant Generator. http:\/\/theory.stanford.edu\/ srirams\/Software\/sting.html \t\t\t\t  2006. StInG: Stanford Invariant Generator. http:\/\/theory.stanford.edu\/ srirams\/Software\/sting.html"},{"key":"e_1_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10373-5_30"},{"key":"e_1_2_1_83_1","unstructured":"2022. Software Verification Competition. https:\/\/sv-comp.sosy-lab.org \t\t\t\t  2022. Software Verification Competition. https:\/\/sv-comp.sosy-lab.org"},{"key":"e_1_2_1_84_1","volume-title":"Complexity Results for Fourier-Motzkin Elimination (Thesis format: Monograph). Ph. D. Dissertation","author":"Talaashrafi Delaram","unstructured":"Delaram Talaashrafi . 2018. Complexity Results for Fourier-Motzkin Elimination (Thesis format: Monograph). Ph. D. Dissertation . The University of Western Ontario London . Delaram Talaashrafi. 2018. Complexity Results for Fourier-Motzkin Elimination (Thesis format: Monograph). Ph. D. Dissertation. The University of Western Ontario London."},{"key":"e_1_2_1_85_1","unstructured":"2021. UltimateAutomizer: A Software Model Checker. https:\/\/monteverdi.informatik.uni-freiburg.de\/tomcat\/Website\/?ui=tool&tool=automizer \t\t\t\t  2021. UltimateAutomizer: A Software Model Checker. https:\/\/monteverdi.informatik.uni-freiburg.de\/tomcat\/Website\/?ui=tool&tool=automizer"},{"key":"e_1_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.1145\/3368089.3409752"},{"key":"e_1_2_1_87_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11704-009-0074-7"},{"key":"e_1_2_1_88_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385986"},{"key":"e_1_2_1_89_1","volume-title":"FM 2012: Formal Methods - 18th International Symposium, Paris, France, August 27-31, 2012. Proceedings, Dimitra Giannakopoulou and Dominique M\u00e9ry (Eds.) (Lecture Notes in Computer Science","volume":"485","author":"Zhao Hengjun","unstructured":"Hengjun Zhao , Naijun Zhan , Deepak Kapur , and Kim G. Larsen . 2012. A \"Hybrid\" Approach for Synthesizing Optimal Controllers of Hybrid Systems: A Case Study of the Oil Pump Industrial Example . In FM 2012: Formal Methods - 18th International Symposium, Paris, France, August 27-31, 2012. Proceedings, Dimitra Giannakopoulou and Dominique M\u00e9ry (Eds.) (Lecture Notes in Computer Science , Vol. 7436). Springer, 471\u2013 485 . Hengjun Zhao, Naijun Zhan, Deepak Kapur, and Kim G. Larsen. 2012. A \"Hybrid\" Approach for Synthesizing Optimal Controllers of Hybrid Systems: A Case Study of the Oil Pump Industrial Example. In FM 2012: Formal Methods - 18th International Symposium, Paris, France, August 27-31, 2012. Proceedings, Dimitra Giannakopoulou and Dominique M\u00e9ry (Eds.) (Lecture Notes in Computer Science, Vol. 7436). Springer, 471\u2013485."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563295","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3563295","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:38:10Z","timestamp":1750178290000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563295"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10,31]]},"references-count":89,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2022,10,31]]}},"alternative-id":["10.1145\/3563295"],"URL":"https:\/\/doi.org\/10.1145\/3563295","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,10,31]]},"assertion":[{"value":"2022-10-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}