{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,18]],"date-time":"2025-12-18T14:28:18Z","timestamp":1766068098439,"version":"3.41.0"},"reference-count":91,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2025,2,17]],"date-time":"2025-02-17T00:00:00Z","timestamp":1739750400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100012166","name":"National Key R&D Program of China","doi-asserted-by":"crossref","award":["2022YFA1005101"],"award-info":[{"award-number":["2022YFA1005101"]}],"id":[{"id":"10.13039\/501100012166","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100001809","name":"Natural Science Foundation of China","doi-asserted-by":"crossref","award":["62192732"],"award-info":[{"award-number":["62192732"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Sponsor National Key R&D Program of China under","award":["2023YFA1009401"],"award-info":[{"award-number":["2023YFA1009401"]}]},{"name":"Sponsor Natural Science Foundation of China under","award":["12201425"],"award-info":[{"award-number":["12201425"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2025,3,31]]},"abstract":"<jats:p>\n            Constraint-solving-based program invariant synthesis takes a parametric invariant template and encodes the (inductive) invariant conditions into constraints. The problem of characterizing the set of all valid parameter assignments is referred to as the\n            <jats:italic>strong invariant synthesis problem<\/jats:italic>\n            , while the problem of finding a concrete valid parameter assignment is called the\n            <jats:italic>weak invariant synthesis problem<\/jats:italic>\n            . For both problems, the challenge lies in solving or reducing the encoded constraints, which are generally non-convex and lack efficient solvers.\n          <\/jats:p>\n          <jats:p>In this article, we propose two novel algorithms for synthesizing invariants of polynomial programs using semidefinite programming (SDP): (1) The Cluster algorithm targets the strong invariant synthesis problem for polynomial invariant templates. Leveraging robust optimization techniques, it solves a series of SDP relaxations and yields a sequence of increasingly precise under-approximations of the set of valid parameter assignments. We prove the algorithm\u2019s soundness, convergence, and weak completeness under a specific robustness assumption on templates. Moreover, the outputs can simplify the weak invariant synthesis problem. (2) The Mask algorithm addresses the weak invariant synthesis problem in scenarios where the aforementioned robustness assumption does not hold, rendering the Cluster algorithm ineffective. It identifies a specific subclass of invariant templates, termed masked templates, involving parameterized polynomial equalities and known inequalities. By applying variable substitution, the algorithm transforms constraints into an equivalent form amenable to SDP relaxations. Both algorithms have been implemented and demonstrated superior performance compared to state-of-the-art methods in our empirical evaluation.<\/jats:p>","DOI":"10.1145\/3708559","type":"journal-article","created":{"date-parts":[[2024,12,18]],"date-time":"2024-12-18T10:16:00Z","timestamp":1734516960000},"page":"1-35","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Synthesizing Invariants for Polynomial Programs by Semidefinite Programming"],"prefix":"10.1145","volume":"47","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9368-4744","authenticated-orcid":false,"given":"Hao","family":"Wu","sequence":"first","affiliation":[{"name":"State Key Lab. of Computer Sciences, Institute of Software, Chinese Academy of Sciences, Beijing, China and University of Chinese Academy of Sciences, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5138-3273","authenticated-orcid":false,"given":"Qiuye","family":"Wang","sequence":"additional","affiliation":[{"name":"State Key Lab. of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China and Fermat Labs, Huawei Inc., Dongguan, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9717-846X","authenticated-orcid":false,"given":"Bai","family":"Xue","sequence":"additional","affiliation":[{"name":"Key Lab. of System Software and State Key Lab. of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China and University of Chinese Academy of Sciences, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3298-3817","authenticated-orcid":false,"given":"Naijun","family":"Zhan","sequence":"additional","affiliation":[{"name":"Key Laboratory of High Confidence Software Technology, School of Computer Science, Peking University, Beijing, China and State Key Lab. of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9973-2217","authenticated-orcid":false,"given":"Lihong","family":"Zhi","sequence":"additional","affiliation":[{"name":"Key Lab. of Mathematics Mechanization, Academy of Mathematics and Systems Science, Chinese Academy of Sciences, Beijing, China and University of Chinese Academy of Sciences, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7489-9237","authenticated-orcid":false,"given":"Zhi-Hong","family":"Yang","sequence":"additional","affiliation":[{"name":"School of Mathematics and Statistics, Central South University, Changsha, China"}]}],"member":"320","published-online":{"date-parts":[[2025,2,17]]},"reference":[{"key":"e_1_3_1_2_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1007\/978-3-662-48288-9_14","volume-title":"22nd International Symposium on Static Analysis","volume":"9291","author":"Adj\u00e9 Assal\u00e9","year":"2015","unstructured":"Assal\u00e9 Adj\u00e9, Pierre-Lo\u00efc Garoche, and Victor Magron. 2015. Property-based polynomial invariant generation using sums-of-squares optimization. In 22nd International Symposium on Static Analysis, Lecture Notes in Computer Science, Vol. 9291. Springer, 235\u2013251. DOI: 10.1007\/978-3-662-48288-9_14"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(1:1)2012"},{"key":"e_1_3_1_4_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1007\/978-3-031-22308-2_3","volume-title":"29th International Symposium on Static Analysis (SAS \u201922)","volume":"13790","author":"Amrollahi Daneshvar","year":"2022","unstructured":"Daneshvar Amrollahi, Ezio Bartocci, George Kenison, Laura Kov\u00e1cs, Marcel Moosbrugger, and Miroslav Stankovic. 2022. Solving invariant generation for unsolvable loops. In 29th International Symposium on Static Analysis (SAS \u201922), Lecture Notes in Computer Science, Vol. 13790. Springer, 19\u201343. DOI: 10.1007\/978-3-031-22308-2_3"},{"key":"e_1_3_1_5_2","doi-asserted-by":"crossref","first-page":"1314","DOI":"10.1109\/CDC45484.2021.9682889","volume-title":"2021 60th IEEE Conference on Decision and Control","author":"Anand Mahathi","year":"2021","unstructured":"Mahathi Anand, Vishnu Murali, Ashutosh Trivedi, and Majid Zamani. 2021. Safety verification of dynamical systems via k-inductive barrier certificates. In 2021 60th IEEE Conference on Decision and Control. IEEE, 1314\u20131320. DOI: 10.1109\/CDC45484.2021.9682889"},{"issue":"2","key":"e_1_3_1_6_2","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1007\/s10107-002-0349-3","article-title":"On implementing a primal-dual interior-point method for conic quadratic optimization","volume":"95","author":"Andersen Erling D.","year":"2003","unstructured":"Erling D. Andersen, Cornelis Roos, and Tam\u00e1s Terlaky. 2003. On implementing a primal-dual interior-point method for conic quadratic optimization. Mathematical Programming 95, 2 (2003), 249\u2013277.","journal-title":"Mathematical Programming"},{"key":"e_1_3_1_7_2","unstructured":"MOSEK ApS. 2019. The MOSEK Optimization Toolbox for MATLAB Manual. Version 9.0. Retrieved from http:\/\/docs.mosek.com\/9.0\/toolbox\/index.html"},{"key":"e_1_3_1_8_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1007\/11547662_4","volume-title":"12th International Symposium on Static Analysis","volume":"3672","author":"Bagnara Roberto","year":"2005","unstructured":"Roberto Bagnara, Enric Rodr\u00edguez-Carbonell, and Enea Zaffanella. 2005. Generation of basic semi-algebraic invariants using convex polyhedra. In 12th International Symposium on Static Analysis (Lecture Notes in Computer Science, Vol. 3672). Springer, 19\u201334. DOI: 10.1007\/11547662_4"},{"key":"e_1_3_1_9_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1007\/978-3-031-13185-1_3","volume-title":"34th International Conference on Computer Aided Verification","volume":"13371","author":"Bao Jialu","year":"2022","unstructured":"Jialu Bao, Nitesh Trivedi, Drashti Pathak, Justin Hsu, and Subhajit Roy. 2022. Data-driven invariant learning for probabilistic programs. In 34th International Conference on Computer Aided Verification, Lecture Notes in Computer Science, Vol. 13371. Springer, Haifa, Israel, 33\u201354. DOI: 10.1007\/978-3-031-13185-1_3"},{"key":"e_1_3_1_10_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"410","DOI":"10.1007\/978-3-031-30820-8_25","volume-title":"29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","volume":"13994","author":"Batz Kevin","year":"2023","unstructured":"Kevin Batz, Mingshuai Chen, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. 2023. Probabilistic program verification via inductive synthesis of inductive invariants. In 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, Vol. 13994. Springer, Paris, France, 410\u2013429. DOI: 10.1007\/978-3-031-30820-8_25"},{"key":"e_1_3_1_11_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"524","DOI":"10.1007\/978-3-030-99524-9_29","volume-title":"28th International Conference Tools and Algorithms for the Construction and Analysis of Systems (TACAS \u201922)","volume":"13243","author":"Blicha Martin","year":"2022","unstructured":"Martin Blicha, Grigory Fedyukovich, Antti E. J. Hyv\u00e4rinen, and Natasha Sharygina. 2022. Transition power abstractions for deep counterexample detection. In 28th International Conference Tools and Algorithms for the Construction and Analysis of Systems (TACAS \u201922), Lecture Notes in Computer Science, Vol. 13243. Springer, 524\u2013542. DOI: 10.1007\/978-3-030-99524-9_29"},{"key":"e_1_3_1_12_2","first-page":"2910","volume-title":"34th IEEE Conference on Decision and Control (CDC)","volume":"3","author":"Blondel Vincent","year":"1995","unstructured":"Vincent Blondel and John N. Tsitsiklis. 1995. NP-hardness of some linear control design problems. In 34th IEEE Conference on Decision and Control (CDC), Vol. 3, 2910\u20132915. DOI: 10.1109\/CDC.1995.478584"},{"key":"e_1_3_1_13_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-03718-8","volume":"36","author":"Bochnak Jacek","year":"1998","unstructured":"Jacek Bochnak, Michel Coste, and Marie-Fran\u00e7oise Roy. 1998. Real Algebraic Geometry, Vol. 36. Springer Science & Business Media.","journal-title":"Real Algebraic Geometry"},{"key":"e_1_3_1_14_2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511804441","volume-title":"Convex Optimization","author":"Boyd Stephen","year":"2004","unstructured":"Stephen Boyd, Stephen P. Boyd, and Lieven Vandenberghe. 2004. Convex Optimization. Cambridge University Press."},{"key":"e_1_3_1_15_2","doi-asserted-by":"crossref","first-page":"672","DOI":"10.1145\/3385412.3385969","volume-title":"41st ACM SIGPLAN International Conference on Programming Language Design and Implementation","author":"Chatterjee Krishnendu","year":"2020","unstructured":"Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady, and Ehsan Kafshdar Goharshady. 2020. Polynomial invariant generation for non-deterministic recursive programs. In 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation. ACM, 672\u2013687. DOI: 10.1145\/3385412.3385969"},{"key":"e_1_3_1_16_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"658","DOI":"10.1007\/978-3-319-21690-4_44","volume-title":"27th International Conference on Computer Aided Verification","volume":"9206","author":"Chen Yu-Fang","year":"2015","unstructured":"Yu-Fang Chen, Chih-Duo Hong, Bow-Yaw Wang, and Lijun Zhang. 2015. Counterexample-guided polynomial loop invariant generation by Lagrange interpolation. In 27th International Conference on Computer Aided Verification, Lecture Notes in Computer Science, Vol. 9206. Springer, San Francisco, CA, 658\u2013674. DOI: 10.1007\/978-3-319-21690-4_44"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0257-4"},{"key":"e_1_3_1_18_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"420","DOI":"10.1007\/978-3-540-45069-6_39","volume-title":"15th International Conference on Computer Aided Verification","volume":"2725","author":"Col\u00f3n Michael","year":"2003","unstructured":"Michael Col\u00f3n, Sriram Sankaranarayanan, and Henny Sipma. 2003. Linear invariant generation using non-linear constraint solving. In 15th International Conference on Computer Aided Verification, Lecture Notes in Computer Science, Vol. 2725. Springer, 420\u2013432. DOI: 10.1007\/978-3-540-45069-6_39"},{"key":"e_1_3_1_19_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-540-30579-8_1","volume-title":"6th International Conference on Verification, Model Checking, and Abstract Interpretation","volume":"3385","author":"Cousot Patrick","year":"2005","unstructured":"Patrick Cousot. 2005. Proving program invariance and termination by parametric abstraction, Lagrangian relaxation and semidefinite programming. In 6th International Conference on Verification, Model Checking, and Abstract Interpretation, Lecture Notes in Computer Science, Vol. 3385. Springer, 1\u201324. DOI: 10.1007\/978-3-540-30579-8_1"},{"key":"e_1_3_1_20_2","first-page":"724","volume-title":"Proceedings of the ACM on Programming Languages","volume":"8","author":"Cyphert John","year":"2024","unstructured":"John Cyphert and Zachary Kincaid. 2024. Solvable polynomial ideals: The ideal reflection for program analysis. Proceedings of the ACM on Programming Languages 8, POPL (2024), 724\u2013752. DOI: 10.1145\/3632867"},{"key":"e_1_3_1_21_2","doi-asserted-by":"crossref","first-page":"62","DOI":"10.1016\/j.jsc.2016.07.010","article-title":"Barrier certificates revisited","volume":"80","author":"Dai Liyun","year":"2017","unstructured":"Liyun Dai, Ting Gan, Bican Xia, and Naijun Zhan. 2017. Barrier certificates revisited. Journal of Symbolic Computation 80 (2017), 62\u201386.","journal-title":"Journal of Symbolic Computation"},{"key":"e_1_3_1_22_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"364","DOI":"10.1007\/978-3-642-39799-8_25","volume-title":"25th International Conference on Computer Aided Verification","volume":"8044","author":"Dai Liyun","year":"2013","unstructured":"Liyun Dai, Bican Xia, and Naijun Zhan. 2013. Generating non-linear interpolants by semidefinite programming. In 25th International Conference on Computer Aided Verification, Lecture Notes in Computer Science, Vol. 8044. Springer, 364\u2013380. DOI: 10.1007\/978-3-642-39799-8_25"},{"issue":"1","key":"e_1_3_1_23_2","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1016\/S0747-7171(88)80004-X","article-title":"Real quantifier elimination is doubly exponential","volume":"5","author":"Davenport James H.","year":"1988","unstructured":"James H. Davenport and Joos Heintz. 1988. Real quantifier elimination is doubly exponential. Journal of Symbolic Computation 5, 1\u20132 (1988), 29\u201335.","journal-title":"Journal of Symbolic Computation"},{"key":"e_1_3_1_24_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","volume":"4963","author":"Moura Leonardo Mendon\u00e7a de","year":"2008","unstructured":"Leonardo Mendon\u00e7a de Moura and Nikolaj S. Bj\u00f8rner. 2008. Z3: An efficient SMT solver. In 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, Vol. 4963. Springer, 337\u2013340. DOI: 10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_1_25_2","doi-asserted-by":"crossref","first-page":"443","DOI":"10.1145\/2509136.2509511","volume-title":"2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications","author":"Dillig Isil","year":"2013","unstructured":"Isil Dillig, Thomas Dillig, Boyang Li, and Kenneth L. McMillan. 2013. Inductive invariant generation via abductive inference. In 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications. ACM, 443\u2013456. DOI: 10.1145\/2509136.2509511"},{"key":"e_1_3_1_26_2","author":"Dolzmann Andreas","year":"1996","unstructured":"Andreas Dolzmann and Thomas Sturm. 1996. Redlog User Manual.","journal-title":"Redlog User Manual"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2015.7542253"},{"key":"e_1_3_1_28_2","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1090\/psapm\/019\/0235771","article-title":"Assigning meanings to programs","volume":"19","author":"Floyd Robert W.","year":"1967","unstructured":"Robert W. Floyd. 1967. Assigning meanings to programs. Mathematical Aspects of Computer Science 19, 19\u201332 (1967), 1.","journal-title":"Mathematical Aspects of Computer Science"},{"key":"e_1_3_1_29_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1007\/978-3-319-40229-1_14","volume-title":"8th International Joint Conference on Automated Reasoning","volume":"9706","author":"Gan Ting","year":"2016","unstructured":"Ting Gan, Liyun Dai, Bican Xia, Naijun Zhan, Deepak Kapur, and Mingshuai Chen. 2016. Interpolant synthesis for quadratic polynomial inequalities and combination with EUF. In 8th International Joint Conference on Automated Reasoning, Lecture Notes in Computer Science, Vol. 9706. Springer, 195\u2013212. DOI: 10.1007\/978-3-319-40229-1_14"},{"key":"e_1_3_1_30_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"415","DOI":"10.1007\/978-3-030-53288-8_20","volume-title":"32nd International Conference on Computer Aided Verification","volume":"12224","author":"Gan Ting","year":"2020","unstructured":"Ting Gan, Bican Xia, Bai Xue, Naijun Zhan, and Liyun Dai. 2020. Nonlinear Craig interpolant generation. In 32nd International Conference on Computer Aided Verification, Lecture Notes in Computer Science, Vol. 12224. Springer, 415\u2013438. DOI: 10.1007\/978-3-030-53288-8_20"},{"key":"e_1_3_1_31_2","first-page":"727","volume-title":"Proceedings of the ACM on Programming Languages","volume":"7","author":"Goharshady Amir Kafshdar","year":"2023","unstructured":"Amir Kafshdar Goharshady, S. Hitarth, Fatemeh Mohammadi, and Harshit J. Motwani. 2023. Algebro-geometric algorithms for template-based synthesis of polynomial programs. Proceedings of the ACM on Programming Languages 7, OOPSLA1 (2023), 727\u2013756. DOI: 10.1145\/3586052"},{"key":"e_1_3_1_32_2","volume-title":"Matrix Computations","author":"Golub Gene H.","year":"1996","unstructured":"Gene H. Golub and Charles F. Van Loan. 1996. Matrix Computations, 3rd ed. Johns Hopkins University Press.","edition":"3"},{"key":"e_1_3_1_33_2","first-page":"1112","volume-title":"41st ACM SIGPLAN International Conference on Programming Language Design and Implementation","author":"He Jingxuan","year":"2020","unstructured":"Jingxuan He, Gagandeep Singh, Markus P\u00fcschel, and Martin T. Vechev. 2020. Learning fast and precise numerical analysis. In 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation. ACM, 1112\u20131127. DOI: 10.1145\/3385412.3386016"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.1080\/10556788.2017.1341505"},{"key":"e_1_3_1_35_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2020.11.001"},{"issue":"10","key":"e_1_3_1_36_2","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","article-title":"An axiomatic basis for computer programming","volume":"12","author":"Hoare Charles Antony Richard","year":"1969","unstructured":"Charles Antony Richard Hoare. 1969. An axiomatic basis for computer programming. Communications of the ACM 12, 10 (1969), 576\u2013580.","journal-title":"Communications of the ACM"},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2018.8603013"},{"key":"e_1_3_1_38_2","first-page":"530","volume-title":"33rd Annual ACM\/IEEE Symposium on Logic in Computer Science","author":"Hrushovski Ehud","year":"2018","unstructured":"Ehud Hrushovski, Jo\u00ebl Ouaknine, Amaury Pouly, and James Worrell. 2018. Polynomial invariants for affine programs. In 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science. ACM, 530\u2013539. DOI: 10.1145\/3209108.3209142"},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/3614319"},{"key":"e_1_3_1_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10107-022-01878-5"},{"key":"e_1_3_1_41_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"226","DOI":"10.1007\/978-3-319-73721-8_11","volume-title":"19th International Conference on Verification, Model Checking, and Abstract Interpretation","volume":"10747","author":"Humenberger Andreas","year":"2018","unstructured":"Andreas Humenberger, Maximilian Jaroschek, and Laura Kov\u00e1cs. 2018. Invariant generation for multi-path loops with polynomial assignments. In 19th International Conference on Verification, Model Checking, and Abstract Interpretation, Lecture Notes in Computer Science, Vol. 10747. Springer, 226\u2013246. DOI: 10.1007\/978-3-319-73721-8_11"},{"key":"e_1_3_1_42_2","first-page":"27","volume-title":"24th IEEE Symposium on Computer Arithmetic","author":"Joldes Mioara","year":"2017","unstructured":"Mioara Joldes, Jean-Michel Muller, and Valentina Popescu. 2017. Implementation and performance evaluation of an extended precision floating-point arithmetic library for high-accuracy semidefinite programming. In 24th IEEE Symposium on Computer Arithmetic. IEEE Computer Society, 27\u201334. DOI: 10.1109\/ARITH.2017.18"},{"key":"e_1_3_1_43_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.JSC.2011.08.002"},{"key":"e_1_3_1_44_2","volume-title":"Deduction and Applications  (Dagstuhl Seminar Proceedings)","volume":"05431","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. Retrieved from http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2006\/511"},{"issue":"2","key":"e_1_3_1_45_2","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1007\/BF00268497","article-title":"Affine relationships among variables of a program","volume":"6","author":"Karr Michael","year":"1976","unstructured":"Michael Karr. 1976. Affine relationships among variables of a program. Acta Informatica 6, 2 (1976), 133\u2013151.","journal-title":"Acta Informatica"},{"key":"e_1_3_1_46_2","first-page":"54:1","volume-title":"Proceedings of the ACM on Programming Languages","volume":"2","author":"Kincaid Zachary","year":"2018","unstructured":"Zachary Kincaid, John Cyphert, Jason Breck, and Thomas W. Reps. 2018. Non-linear reasoning for invariant synthesis. Proceedings of the ACM on Programming Languages 2, POPL (2018), 54:1\u201354:33. DOI: 10.1145\/3158142"},{"key":"e_1_3_1_47_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"338","DOI":"10.1007\/978-3-030-99524-9_18","volume-title":"28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","volume":"13243","author":"Koenig Jason R.","year":"2022","unstructured":"Jason R. Koenig, Oded Padon, Sharon Shoham, and Alex Aiken. 2022. Inferring invariants with quantifier alternations: Taming the search space explosion. In 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, Vol. 13243. Springer, 338\u2013356. DOI: 10.1007\/978-3-030-99524-9_18"},{"key":"e_1_3_1_48_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1007\/978-3-319-08867-9_2","volume-title":"26th International Conference on Computer Aided Verification (CAV \u201914)","volume":"8559","author":"Komuravelli Anvesh","year":"2014","unstructured":"Anvesh Komuravelli, Arie Gurfinkel, and Sagar Chaki. 2014. SMT-based model checking for recursive programs. In 26th International Conference on Computer Aided Verification (CAV \u201914), Lecture Notes in Computer Science, Vol. 8559. Springer, 17\u201334. DOI: 10.1007\/978-3-319-08867-9_2"},{"key":"e_1_3_1_49_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1007\/978-3-540-78800-3_18","volume-title":"14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS \u201908)","volume":"4963","author":"Kov\u00e1cs Laura","year":"2008","unstructured":"Laura Kov\u00e1cs. 2008. Reasoning algebraically about P-solvable loops. In 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS \u201908), Lecture Notes in Computer Science, Vol. 4963. Springer, 249\u2013264. DOI: 10.1007\/978-3-540-78800-3_18"},{"key":"e_1_3_1_50_2","doi-asserted-by":"crossref","first-page":"796","DOI":"10.1137\/S1052623400366802","article-title":"Global optimization with polynomials and the problem of moments","volume":"11","author":"Lasserre Jean Bernard","year":"2000","unstructured":"Jean Bernard Lasserre. 2000. Global optimization with polynomials and the problem of moments. SIAM Journal on Optimization 11 (2000), 796\u2013817. Retrieved from https:\/\/api.semanticscholar.org\/CorpusID:16740871","journal-title":"SIAM Journal on Optimization"},{"key":"e_1_3_1_51_2","doi-asserted-by":"crossref","DOI":"10.1142\/p665","volume":"1","author":"Lasserre Jean Bernard","year":"2009","unstructured":"Jean Bernard Lasserre. 2009. Moments, Positive Polynomials and Their Applications, Vol. 1. World Scientific.","journal-title":"Moments, Positive Polynomials and Their Applications"},{"issue":"2","key":"e_1_3_1_52_2","doi-asserted-by":"crossref","first-page":"507","DOI":"10.1007\/s10107-014-0838-1","article-title":"Tractable approximations of sets defined with quantifiers","volume":"151","author":"Lasserre Jean B.","year":"2015","unstructured":"Jean B. Lasserre. 2015. Tractable approximations of sets defined with quantifiers. Mathematical Programming 151, 2 (2015), 507\u2013527.","journal-title":"Mathematical Programming"},{"key":"e_1_3_1_53_2","doi-asserted-by":"publisher","DOI":"10.1137\/090775221"},{"key":"e_1_3_1_54_2","doi-asserted-by":"crossref","first-page":"407","DOI":"10.1007\/978-1-4614-0769-0_14","volume-title":"Handbook on Semidefinite, Conic and Polynomial Optimization","author":"Lasserre Jean B.","year":"2012","unstructured":"Jean B. Lasserre and Mihai Putinar. 2012. Positivity and optimization: Beyond polynomials. In Handbook on Semidefinite, Conic and Polynomial Optimization. Miguel F. Anjos and Jean B. Lasserre (Eds.), Springer, 407\u2013434."},{"key":"e_1_3_1_55_2","first-page":"793","volume-title":"32nd IEEE\/ACM International Conference on Automated Software Engineering","author":"Lin Shang-Wei","year":"2017","unstructured":"Shang-Wei Lin, Jun Sun, Hao Xiao, Yang Liu, David San\u00e1n, and Henri Hansen. 2017. FiB: Squeezing loop invariants by interpolation between forward\/backward predicate transformers. In 32nd IEEE\/ACM International Conference on Automated Software Engineering. IEEE Computer Society, 793\u2013803. DOI: 10.1109\/ASE.2017.8115690"},{"key":"e_1_3_1_56_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11704-014-3150-6"},{"key":"e_1_3_1_57_2","first-page":"204","volume-title":"Proceedings of the ACM on Programming Languages","volume":"6","author":"Liu Hongming","year":"2022","unstructured":"Hongming Liu, Hongfei Fu, Zhiyong Yu, Jiaxin Song, and Guoqiang Li. 2022. Scalable linear invariant generation with Farkas\u2019 lemma. Proceedings of the ACM on Programming Languages 6, OOPSLA2 (2022), 204\u2013232. DOI: 10.1145\/3563295"},{"key":"e_1_3_1_58_2","first-page":"284","volume-title":"2004 IEEE International Symposium on Computer Aided Control Systems Design (CACSD \u201904)","author":"L\u00f6fberg J.","year":"2004","unstructured":"J. L\u00f6fberg. 2004. YALMIP: A toolbox for modeling and optimization in MATLAB. In 2004 IEEE International Symposium on Computer Aided Control Systems Design (CACSD \u201904), 284\u2013289."},{"key":"e_1_3_1_59_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10107-021-01634-1"},{"key":"e_1_3_1_60_2","doi-asserted-by":"crossref","DOI":"10.1090\/surv\/146","volume-title":"Positive Polynomials and Sums of Squares","author":"Marshall Murray","year":"2008","unstructured":"Murray Marshall. 2008. Positive Polynomials and Sums of Squares. Number 146. American Mathematical Soc."},{"key":"e_1_3_1_61_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"15th International Conference on Computer Aided Verification (CAV 2003)","volume":"2725","author":"McMillan Kenneth L.","year":"2003","unstructured":"Kenneth L. McMillan. 2003. Interpolation and SAT-based model checking. In 15th International Conference on Computer Aided Verification (CAV 2003), Lecture Notes in Computer Science, Vol. 2725. Springer, 1\u201313. DOI: 10.1007\/978-3-540-45069-6_1"},{"key":"e_1_3_1_62_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/11817963_14","volume-title":"18th International Conference on Computer Aided Verification (CAV \u201906)","volume":"4144","author":"McMillan Kenneth L.","year":"2006","unstructured":"Kenneth L. McMillan. 2006. Lazy abstraction with interpolants. In 18th International Conference on Computer Aided Verification (CAV \u201906), Lecture Notes in Computer Science, Vol. 4144. Springer, 123\u2013136. DOI: 10.1007\/11817963_14"},{"key":"e_1_3_1_63_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2004.05.004"},{"key":"e_1_3_1_64_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27836-8_85"},{"key":"e_1_3_1_65_2","first-page":"882","volume-title":"Proceedings of the ACM on Programming Languages","volume":"8","author":"M\u00fcllner Julian","year":"2024","unstructured":"Julian M\u00fcllner, Marcel Moosbrugger, and Laura Kov\u00e1cs. 2024. Strong invariants are hard: On the hardness of strongest polynomial invariants for (probabilistic) programs. Proceedings of the ACM on Programming Languages 8, POPL (2024), 882\u2013910. DOI: 10.1145\/3632872"},{"issue":"4","key":"e_1_3_1_66_2","doi-asserted-by":"crossref","first-page":"310","DOI":"10.1007\/BF01966091","article-title":"Proof of algorithms by general snapshots","volume":"6","author":"Naur Peter","year":"1966","unstructured":"Peter Naur. 1966. Proof of algorithms by general snapshots. BIT Numerical Mathematics 6, 4 (1966), 310\u2013316.","journal-title":"BIT Numerical Mathematics"},{"key":"e_1_3_1_67_2","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1007\/s10107-013-0680-x","article-title":"Optimality conditions and finite convergence of Lasserre\u2019s hierarchy","volume":"146","author":"Nie Jiawang","year":"2014","unstructured":"Jiawang Nie. 2014. Optimality conditions and finite convergence of Lasserre\u2019s hierarchy. Mathematical Programming 146 (2014), 97\u2013121.","journal-title":"Mathematical Programming"},{"key":"e_1_3_1_68_2","first-page":"1","volume-title":"Proceedings of the ACM on Programming Languages","volume":"6","author":"Padon Oded","year":"2022","unstructured":"Oded Padon, James R. Wilcox, Jason R. Koenig, Kenneth L. McMillan, and Alex Aiken. 2022. Induction duality: Primal-dual search for invariants. Proceedings of the ACM on Programming Languages 6, POPL (2022), 1\u201329. DOI: 10.1145\/3498712"},{"key":"e_1_3_1_69_2","volume-title":"Structured Semidefinite Programs and Semialgebraic Geometry Methods in Robustness and Optimization","author":"Parrilo Pablo A.","year":"2000","unstructured":"Pablo A. Parrilo. 2000. Structured Semidefinite Programs and Semialgebraic Geometry Methods in Robustness and Optimization. California Institute of Technology."},{"issue":"3","key":"e_1_3_1_70_2","doi-asserted-by":"crossref","first-page":"969","DOI":"10.1512\/iumj.1993.42.42045","article-title":"Positive polynomials on compact semi-algebraic sets","volume":"42","author":"Putinar Mihai","year":"1993","unstructured":"Mihai Putinar. 1993. Positive polynomials on compact semi-algebraic sets. Indiana University Mathematics Journal 42, 3 (1993), 969\u2013984.","journal-title":"Indiana University Mathematics Journal"},{"key":"e_1_3_1_71_2","unstructured":"Enric Rodr\u00edguez-Carbonell. 2016. Some Programs That Need Polynomial Invariants in Order to Be Verified. Retrieved from https:\/\/www.cs.upc.edu\/erodri\/webpage\/polynomial_invariants\/list.html"},{"key":"e_1_3_1_72_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"280","DOI":"10.1007\/978-3-540-27864-1_21","volume-title":"11th International Symposium on Static Analysis","volume":"3148","author":"Rodr\u00edguez-Carbonell Enric","year":"2004","unstructured":"Enric Rodr\u00edguez-Carbonell and Deepak Kapur. 2004. An abstract interpretation approach for automatic generation of polynomial invariants. In 11th International Symposium on Static Analysis, Lecture Notes in Computer Science, Vol. 3148. Springer, 280\u2013295. DOI: 10.1007\/978-3-540-27864-1_21"},{"key":"e_1_3_1_73_2","doi-asserted-by":"crossref","first-page":"266","DOI":"10.1145\/1005285.1005324","volume-title":"2004 International Symposium on Symbolic and Algebraic Computation","author":"Rodr\u00edguez-Carbonell Enric","year":"2004","unstructured":"Enric Rodr\u00edguez-Carbonell and Deepak Kapur. 2004. Automatic generation of polynomial loop invariants: Algebraic foundations. In 2004 International Symposium on Symbolic and Algebraic Computation, 266\u2013273."},{"issue":"1","key":"e_1_3_1_74_2","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1016\/j.scico.2006.03.003","article-title":"Automatic generation of polynomial invariants of bounded degree using abstract interpretation","volume":"64","author":"Rodr\u00edguez-Carbonell Enric","year":"2007","unstructured":"Enric Rodr\u00edguez-Carbonell and Deepak Kapur. 2007. Automatic generation of polynomial invariants of bounded degree using abstract interpretation. Science of Computer Programming 64, 1 (2007), 54\u201375.","journal-title":"Science of Computer Programming"},{"issue":"4","key":"e_1_3_1_75_2","doi-asserted-by":"crossref","first-page":"443","DOI":"10.1016\/j.jsc.2007.01.002","article-title":"Generating all polynomial invariants in simple loops","volume":"42","author":"Rodr\u00edguez-Carbonell Enric","year":"2007","unstructured":"Enric Rodr\u00edguez-Carbonell and Deepak Kapur. 2007. Generating all polynomial invariants in simple loops. Journal of Symbolic Computation 42, 4 (2007), 443\u2013476.","journal-title":"Journal of Symbolic Computation"},{"issue":"2","key":"e_1_3_1_76_2","doi-asserted-by":"crossref","first-page":"286","DOI":"10.1007\/s10703-017-0302-y","article-title":"Validating numerical semidefinite programming solvers for polynomial invariants","volume":"53","author":"Roux Pierre","year":"2018","unstructured":"Pierre Roux, Yuen-Lam Voronin, and Sriram Sankaranarayanan. 2018. Validating numerical semidefinite programming solvers for polynomial invariants. Formal Methods in System Design 53, 2 (2018), 286\u2013312.","journal-title":"Formal Methods in System Design"},{"key":"e_1_3_1_77_2","doi-asserted-by":"publisher","DOI":"10.1137\/0203021"},{"key":"e_1_3_1_78_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"539","DOI":"10.1007\/978-3-540-24743-2_36","volume-title":"7th International Workshop on Hybrid Systems: Computation and Control","volume":"2993","author":"Sankaranarayanan Sriram","year":"2004","unstructured":"Sriram Sankaranarayanan, Henny Sipma, and Zohar Manna. 2004. Constructing invariants for hybrid systems. In 7th International Workshop on Hybrid Systems: Computation and Control, Lecture Notes in Computer Science, Vol. 2993. Springer, 539\u2013554. DOI: 10.1007\/978-3-540-24743-2_36"},{"key":"e_1_3_1_79_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/978-3-540-27864-1_7","volume-title":"11th International Symposium on Static Analysis","volume":"3148","author":"Sankaranarayanan Sriram","year":"2004","unstructured":"Sriram Sankaranarayanan, Henny B. Sipma, and Zohar Manna. 2004. Constraint-based linear-relations analysis. In 11th International Symposium on Static Analysis, Lecture Notes in Computer Science, Vol. 3148. Springer, 53\u201368. DOI: 10.1007\/978-3-540-27864-1_7"},{"issue":"4","key":"e_1_3_1_80_2","doi-asserted-by":"crossref","first-page":"506","DOI":"10.1016\/j.sysconle.2012.01.004","article-title":"Controller synthesis for robust invariance of polynomial dynamical systems using linear programming","volume":"61","author":"Sassi Mohamed Amin Ben","year":"2012","unstructured":"Mohamed Amin Ben Sassi and Antoine Girard. 2012. Controller synthesis for robust invariance of polynomial dynamical systems using linear programming. Systems & Control Letters 61, 4 (2012), 506\u2013512.","journal-title":"Systems & Control Letters"},{"key":"e_1_3_1_81_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"88","DOI":"10.1007\/978-3-319-08867-9_6","volume-title":"26th International Conference on Computer Aided Verification","volume":"8559","author":"Sharma Rahul","year":"2014","unstructured":"Rahul Sharma and Alex Aiken. 2014. From invariant checking to invariant inference using randomized search. In 26th International Conference on Computer Aided Verification, Lecture Notes in Computer Science, Vol. 8559. Springer, 88\u2013105. DOI: 10.1007\/978-3-319-08867-9_6"},{"key":"e_1_3_1_82_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1007\/978-3-030-53291-8_9","volume-title":"32nd International Conference on Computer Aided Verification","volume":"12225","author":"Si Xujie","year":"2020","unstructured":"Xujie Si, Aaditya Naik, Hanjun Dai, Mayur Naik, and Le Song. 2020. Code2Inv: A deep learning framework for program verification. In 32nd International Conference on Computer Aided Verification, Lecture Notes in Computer Science, Vol. 12225. Springer, 151\u2013164. DOI: 10.1007\/978-3-030-53291-8_9"},{"key":"e_1_3_1_83_2","doi-asserted-by":"crossref","DOI":"10.1525\/9780520348097","volume-title":"A Decision Method for Elementary Algebra and Geometry","author":"Tarski Alfred","year":"1951","unstructured":"Alfred Tarski. 1951. A Decision Method for Elementary Algebra and Geometry. University of California Press, Berkeley."},{"key":"e_1_3_1_84_2","first-page":"2525","volume-title":"the American Control Conference (ACC)","volume":"4","author":"Toker Onur","year":"1995","unstructured":"Onur Toker and Hitay \u00d6zbay. 1995. On the NP-hardness of solving bilinear matrix inequalities and simultaneous stabilization with static output feedback. In the American Control Conference (ACC), Vol. 4, 2525\u20132526. DOI: 10.1109\/ACC.1995.532300"},{"key":"e_1_3_1_85_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"409","DOI":"10.1007\/978-3-031-65627-9_20","volume-title":"36th International Conference on Computer Aided Verification (CAV \u201924)","volume":"14681","author":"Wang Chenglin","year":"2024","unstructured":"Chenglin Wang and Fangzhen Lin. 2024. On polynomial expressions with C-finite recurrences in loops with nested nondeterministic branches. In 36th International Conference on Computer Aided Verification (CAV \u201924), Lecture Notes in Computer Science, Vol. 14681. Springer, 409\u2013430. DOI: 10.1007\/978-3-031-65627-9_20"},{"key":"e_1_3_1_86_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"443","DOI":"10.1007\/978-3-030-81685-8_21","volume-title":"33rd International Conference on Computer Aided Verification (CAV \u201921)","volume":"12759","author":"Wang Qiuye","year":"2021","unstructured":"Qiuye Wang, Mingshuai Chen, Bai Xue, Naijun Zhan, and Joost-Pieter Katoen. 2021. Synthesizing invariant barrier certificates via difference-of-convex programming. In 33rd International Conference on Computer Aided Verification (CAV \u201921), Lecture Notes in Computer Science, Vol. 12759. Springer, 443\u2013466."},{"key":"e_1_3_1_87_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2022.104965"},{"key":"e_1_3_1_88_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"248","DOI":"10.1007\/978-3-031-71177-0_16","volume-title":"26th International Symposium on Formal Methods (FM (2))","volume":"14934","author":"Wu Hao","year":"2024","unstructured":"Hao Wu, Shenghua Feng, Ting Gan, Jie Wang, Bican Xia, and Naijun Zhan. 2024. On completeness of SDP-based barrier certificate synthesis over unbounded domains. In 26th International Symposium on Formal Methods (FM (2)), Lecture Notes in Computer Science, Vol. 14934. Springer, 248\u2013266. DOI: 10.1007\/978-3-031-71177-0_16"},{"key":"e_1_3_1_89_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"92","DOI":"10.1007\/978-3-031-71162-6_5","volume-title":"26th International Symposium on Formal Methods (FM (1))","volume":"14933","author":"Wu Hao","year":"2024","unstructured":"Hao Wu, Jie Wang, Bican Xia, Xiakun Li, Naijun Zhan, and Ting Gan. 2024. Nonlinear Craig interpolant generation over unbounded domains by separating semialgebraic sets. In 26th International Symposium on Formal Methods (FM (1)), Lecture Notes in Computer Science, Vol. 14933. Springer, 92\u2013110. DOI: 10.1007\/978-3-031-71162-6_5"},{"key":"e_1_3_1_90_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11704-009-0074-7"},{"key":"e_1_3_1_91_2","first-page":"106","volume-title":"41st ACM SIGPLAN Conference on Programming Language Design and Implementation","author":"Yao Jianan","year":"2020","unstructured":"Jianan Yao, Gabriel Ryan, Justin Wong, Suman Jana, and Ronghui Gu. 2020. Learning nonlinear loop invariants with gated continuous logic networks. In 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, 106\u2013120."},{"key":"e_1_3_1_92_2","first-page":"175","volume-title":"32nd ACM SIGSOFT International Symposium on Software Testing and Analysis","author":"Yu Shiwen","year":"2023","unstructured":"Shiwen Yu, Ting Wang, and Ji Wang. 2023. Loop invariant inference through SMT solving enhanced reinforcement learning. In 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis. ACM, 175\u2013187. DOI: 10.1145\/3597926.3598047"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3708559","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3708559","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:17:47Z","timestamp":1750295867000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3708559"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,2,17]]},"references-count":91,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2025,3,31]]}},"alternative-id":["10.1145\/3708559"],"URL":"https:\/\/doi.org\/10.1145\/3708559","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"type":"print","value":"0164-0925"},{"type":"electronic","value":"1558-4593"}],"subject":[],"published":{"date-parts":[[2025,2,17]]},"assertion":[{"value":"2023-08-23","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-30","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-02-17","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}