{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,25]],"date-time":"2026-09-25T19:50:19Z","timestamp":1790365819840,"version":"4.1.0"},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"5s","license":[{"start":{"date-parts":[[2017,9,27]],"date-time":"2017-09-27T00:00:00Z","timestamp":1506470400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Complex Systems Engineering academic research chair"},{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["ANR-13-INSE-003, ANR-12-INSE-007"],"award-info":[{"award-number":["ANR-13-INSE-003, ANR-12-INSE-007"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]},{"name":"PGMO"},{"name":"ICODE"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2017,10,31]]},"abstract":"<jats:p>We introduce a new method to compute non-convex invariants of numerical programs, which includes the class of switched affine systems with affine guards. We obtain disjunctive and non-convex invariants by associating different partial execution traces with different ellipsoids. A key ingredient is the solution of non-monotone fixed points problems over the space of ellipsoids with a reduction to small size linear matrix inequalities. This allows us to analyze instances that are inaccessible in terms of expressivity or scale by earlier methods based on semi-definite programming.<\/jats:p>","DOI":"10.1145\/3126502","type":"journal-article","created":{"date-parts":[[2017,9,27]],"date-time":"2017-09-27T12:33:53Z","timestamp":1506515633000},"page":"1-19","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["A Fast Method to Compute Disjunctive Quadratic Invariants of Numerical Programs"],"prefix":"10.1145","volume":"16","author":[{"given":"Xavier","family":"Allamigeon","sequence":"first","affiliation":[{"name":"INRIA and CMAP, \u00c9cole polytechnique, CNRS, \u00c9cole polytechnique, Palaiseau"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"St\u00e9phane","family":"Gaubert","sequence":"additional","affiliation":[{"name":"INRIA and CMAP, \u00c9cole polytechnique, CNRS, \u00c9cole polytechnique, Palaiseau"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Eric","family":"Goubault","sequence":"additional","affiliation":[{"name":"LIX, \u00c9cole polytechnique, CNRS, \u00c9cole polytechnique, Palaiseau"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sylvie","family":"Putot","sequence":"additional","affiliation":[{"name":"LIX, \u00c9cole polytechnique, CNRS, \u00c9cole polytechnique, Palaiseau"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nikolas","family":"Stott","sequence":"additional","affiliation":[{"name":"INRIA and CMAP, \u00c9cole polytechnique, CNRS"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2017,9,27]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46081-8_6"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_3"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1137\/110855272"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2932187"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.laa.2013.08.006"},{"key":"e_1_2_1_6_1","doi-asserted-by":"crossref","unstructured":"A. Ben-Tal and A. S. Nemirovskiaei. 2001. Lectures on Modern Convex Optimization: Analysis Algorithms and Engineering Applications. Society for Industrial and Applied Mathematics Philadelphia PA USA.   A. Ben-Tal and A. S. Nemirovskiaei. 2001. Lectures on Modern Convex Optimization: Analysis Algorithms and Engineering Applications. Society for Industrial and Applied Mathematics Philadelphia PA USA.","DOI":"10.1137\/1.9780898718829"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1287\/opre.29.6.1039"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0005-1098(00)00050-9"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1137\/080731347"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000496"},{"key":"e_1_2_1_11_1","volume-title":"Linear Matrix Inequalities in System and Control Theory. Studies in Applied Mathematics","volume":"15","author":"Boyd S.","unstructured":"S. Boyd , L. El Ghaoui , E. Feron , and V. Balakrishnan . 1994 . Linear Matrix Inequalities in System and Control Theory. Studies in Applied Mathematics , Vol. 15 . SIAM, Philadelphia, PA. S. Boyd, L. El Ghaoui, E. Feron, and V. Balakrishnan. 1994. Linear Matrix Inequalities in System and Control Theory. Studies in Applied Mathematics, Vol. 15. SIAM, Philadelphia, PA."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/9.664150"},{"key":"e_1_2_1_13_1","volume-title":"The foundations of minkowskian geometry.Commentarii mathematici Helvetici 24","author":"Busemann H.","year":"1950","unstructured":"H. Busemann . 1950. The foundations of minkowskian geometry.Commentarii mathematici Helvetici 24 ( 1950 ), 156--187. http:\/\/eudml.org\/doc\/139004 H. Busemann. 1950. The foundations of minkowskian geometry.Commentarii mathematici Helvetici 24 (1950), 156--187. http:\/\/eudml.org\/doc\/139004"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_1"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512770"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1137\/15M103114X"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96725"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24725-8_4"},{"key":"e_1_2_1_20_1","unstructured":"E. Feron and F. Alegre. 2008. Control software analysis part I Open-loop properties. CoRR abs\/0809.4812 (2008).  E. Feron and F. Alegre. 2008. Control software analysis part I Open-loop properties. CoRR abs\/0809.4812 (2008)."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2011.12.048"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(97)00034-8"},{"key":"e_1_2_1_23_1","unstructured":"E. Goubault and S. Putot. 2009. A zonotopic framework for functional abstractions. CoRR abs\/0910.1763 (2009).  E. Goubault and S. Putot. 2009. A zonotopic framework for functional abstractions. CoRR abs\/0910.1763 (2009)."},{"key":"e_1_2_1_24_1","volume-title":"PENLAB: A MATLAB solver for nonlinear semidefinite optimization.","author":"Fiala M. Stingl J.","year":"2013","unstructured":"M. Stingl J. Fiala , M. Ko\u010bvara . 2013 . PENLAB: A MATLAB solver for nonlinear semidefinite optimization. (2013). M. Stingl J. Fiala, M. Ko\u010bvara. 2013. PENLAB: A MATLAB solver for nonlinear semidefinite optimization. (2013)."},{"key":"e_1_2_1_25_1","volume-title":"6th International Symposium, SAS\u201999","author":"Jeannet B.","year":"1999","unstructured":"B. Jeannet , N. Halbwachs , and P. Raymond . 1999. Dynamic partitioning in analyses of numerical properties. In Static Analysis , 6th International Symposium, SAS\u201999 , Venice, Italy , September 22-24, 1999 , Proceedings. 39--50. B. Jeannet, N. Halbwachs, and P. Raymond. 1999. Dynamic partitioning in analyses of numerical properties. In Static Analysis, 6th International Symposium, SAS\u201999, Venice, Italy, September 22-24, 1999, Proceedings. 39--50."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9939-1951-0042064-2"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/CACSD.2004.1393890"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/SCAM.2003.1238027"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31987-0_2"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/11609773_23"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2004.05.004"},{"key":"e_1_2_1_33_1","volume-title":"Conference of Decision and Control.","author":"Nilsson P.","unstructured":"P. Nilsson , U. Boscain , M. Sigalotti , and J. Newling . 2013. Invariant sets of defocused switched systems . In Conference of Decision and Control. P. Nilsson, U. Boscain, M. Sigalotti, and J. Newling. 2013. Invariant sets of defocused switched systems. In Conference of Decision and Control."},{"key":"e_1_2_1_34_1","doi-asserted-by":"crossref","unstructured":"M. Oulamara and A. J. Venet. 2015. CAV 2015 San Francisco CA USA July 18-24 2015 Proceedings Part I. Springer International Publishing Cham Chapter Abstract Interpretation with Higher-Dimensional Ellipsoids and Conic Extrapolation 415--430.  M. Oulamara and A. J. Venet. 2015. CAV 2015 San Francisco CA USA July 18-24 2015 Proceedings Part I. Springer International Publishing Cham Chapter Abstract Interpretation with Higher-Dimensional Ellipsoids and Conic Extrapolation 415--430.","DOI":"10.1007\/978-3-319-21690-4_24"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2006.03.003"},{"key":"e_1_2_1_36_1","volume-title":"ATVA (Lecture Notes in Computer Science)","author":"Roux P.","unstructured":"P. Roux and P.-L. Garoche . 2013. Integrating policy iterations in abstract interpreters . In ATVA (Lecture Notes in Computer Science) , D. Van Hung and M. Ogawa (Eds.), Vol. 8172 . Springer , 240--254. P. Roux and P.-L. Garoche. 2013. Integrating policy iterations in abstract interpreters. In ATVA (Lecture Notes in Computer Science), D. Van Hung and M. Ogawa (Eds.), Vol. 8172. Springer, 240--254."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2185632.2185651"},{"key":"e_1_2_1_38_1","volume-title":"Validating Numerical Semidefinite Programming Solvers for Polynomial Invariants","author":"Roux Pierre","unstructured":"Pierre Roux , Yuen-Lam Voronin , and Sriram Sankaranarayanan . 2016. Validating Numerical Semidefinite Programming Solvers for Polynomial Invariants . Springer Berlin Heidelberg , Berlin, Heidelberg , 424--446. Pierre Roux, Yuen-Lam Voronin, and Sriram Sankaranarayanan. 2016. Validating Numerical Semidefinite Programming Solvers for Polynomial Invariants. Springer Berlin Heidelberg, Berlin, Heidelberg, 424--446."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_2"},{"key":"e_1_2_1_40_1","doi-asserted-by":"crossref","unstructured":"P. Sotin B. Jeannet F. V\u00e9drine and E. Goubault. 2011. Policy Iteration within Logico-Numerical Abstract Domains. 290--305.   P. Sotin B. Jeannet F. V\u00e9drine and E. Goubault. 2011. Policy Iteration within Logico-Numerical Abstract Domains. 290--305.","DOI":"10.1007\/978-3-642-24372-1_21"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10107-002-0347-5"},{"key":"e_1_2_1_42_1","volume-title":"Third International Symposium, SAS\u201996","author":"Venet A.","year":"1996","unstructured":"A. Venet . 1996 . Abstract cofibered domains: Application to the alias analysis of untyped programs. In Static Analysis , Third International Symposium, SAS\u201996 , Aachen, Germany , September 24-26, 1996, Proceedings. 366--382. A. Venet. 1996. Abstract cofibered domains: Application to the alias analysis of untyped programs. In Static Analysis, Third International Symposium, SAS\u201996, Aachen, Germany, September 24-26, 1996, Proceedings. 366--382."},{"key":"e_1_2_1_43_1","volume-title":"9th International Symposium, SAS 2002, Madrid, Spain, September 17-20, 2002, Proceedings. 36--51","author":"Venet A.","year":"2002","unstructured":"A. Venet . 2002 . Nonuniform alias analysis of recursive data structures and arrays. In Static Analysis , 9th International Symposium, SAS 2002, Madrid, Spain, September 17-20, 2002, Proceedings. 36--51 . A. Venet. 2002. Nonuniform alias analysis of recursive data structures and arrays. In Static Analysis, 9th International Symposium, SAS 2002, Madrid, Spain, September 17-20, 2002, Proceedings. 36--51."}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3126502","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3126502","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:05:01Z","timestamp":1750273501000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3126502"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,9,27]]},"references-count":42,"journal-issue":{"issue":"5s","published-print":{"date-parts":[[2017,10,31]]}},"alternative-id":["10.1145\/3126502"],"URL":"https:\/\/doi.org\/10.1145\/3126502","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"value":"1539-9087","type":"print"},{"value":"1558-3465","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,9,27]]},"assertion":[{"value":"2017-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-09-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}