{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T00:48:13Z","timestamp":1775868493531,"version":"3.50.1"},"reference-count":42,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,1,19]],"date-time":"2012-01-19T00:00:00Z","timestamp":1326931200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We introduce a new domain for finding precise numerical invariants of\nprograms by abstract interpretation. This domain, which consists of level sets\nof non-linear functions, generalizes the domain of linear \"templates\"\nintroduced by Manna, Sankaranarayanan, and Sipma. In the case of quadratic\ntemplates, we use Shor's semi-definite relaxation to derive computable yet\nprecise abstractions of semantic functionals, and we show that the abstract\nfixpoint equation can be solved accurately by coupling policy iteration and\nsemi-definite programming. We demonstrate the interest of our approach on a\nseries of examples (filters, integration schemes) including a degenerate one\n(symplectic scheme).<\/jats:p>","DOI":"10.2168\/lmcs-8(1:1)2012","type":"journal-article","created":{"date-parts":[[2012,9,6]],"date-time":"2012-09-06T10:03:11Z","timestamp":1346925791000},"source":"Crossref","is-referenced-by-count":17,"title":["Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis"],"prefix":"10.46298","volume":"Volume 8, Issue 1","author":[{"given":"Assal\u00e9","family":"Adj\u00e9","sequence":"first","affiliation":[]},{"given":"St\u00e9phane","family":"Gaubert","sequence":"additional","affiliation":[]},{"given":"Eric","family":"Goubault","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2012,1,19]]},"reference":[{"key":"10.2168\/LMCS-8(1:1)2012_adjephd","unstructured":"A. Adj\u00e9.Optimisation et jeux appliqu\u00e9s \u00e0 l'analyse statique de programme par interpr\u00e9tation abstraite. Phd thesis, \u00c9cole Polytechnique, April 2011."},{"key":"10.2168\/LMCS-8(1:1)2012_Policy2","unstructured":"A. Adje, S. Gaubert, and E. Goubault. Computing the smallest fixed point of nonexpansive mappings arising in game theory and static analysis of programs. Technical report, arXiv:0806.1160, Proceedings of MTNS'08, Blacksburg, Virginia, July 2008."},{"key":"10.2168\/LMCS-8(1:1)2012_adjegaubertgoubault10","doi-asserted-by":"crossref","unstructured":"A. Adje, S. Gaubert, and E. Goubault. Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis. InProceedings of the 19th European Symposium on Programming (ESOP 2010), number 6012 in Lecture Notes in Computer Science, pages 23-42. Springer, 2010.","DOI":"10.1007\/978-3-642-11957-6_3"},{"key":"10.2168\/LMCS-8(1:1)2012_AuTe","unstructured":"A. Auslender and M. Teboulle.Asymptotic Cones and Functions in Optimization and Variational Inequalities. Springer, 2003."},{"key":"10.2168\/LMCS-8(1:1)2012_BagnaraR-CZ05","doi-asserted-by":"crossref","unstructured":"R. Bagnara, E. Rodr\u00edguez-Carbonell, and E. Zaffanella. Generation of basic semi-algebraic invariants using convex polyhedra. In C. Hankin, editor,Static Analysis: Proceedings of the 12th International Symposium, volume 3672 ofLNCS, pages 19-34. Springer, 2005.","DOI":"10.1007\/11547662_4"},{"key":"10.2168\/LMCS-8(1:1)2012_CC77","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"10.2168\/LMCS-8(1:1)2012_Policy1","doi-asserted-by":"crossref","unstructured":"A. Costan, S. Gaubert, E. Goubault, M. Martel, and S. Putot. A policy iteration algorithm for computing fixed points in static analysis of programs. InProceedings of the 17th International Conference on Computer Aided Verification (CAV'05), volume 3576 ofLNCS, pages 462-475. Springer, 2005.","DOI":"10.1007\/11513988_46"},{"key":"10.2168\/LMCS-8(1:1)2012_CousotLagrange","doi-asserted-by":"crossref","unstructured":"P. Cousot. Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming. InSixth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'05), volume 3385 ofLNCS, pages 1-24. Springer, 2005.","DOI":"10.1007\/978-3-540-30579-8_1"},{"key":"10.2168\/LMCS-8(1:1)2012_priestley","doi-asserted-by":"crossref","unstructured":"B. A. Davey and H. A. Priestley.Introduction to lattices and order. Cambridge University Press, New York, second edition, 2002.","DOI":"10.1017\/CBO9780511809088"},{"key":"10.2168\/LMCS-8(1:1)2012_Feron2","unstructured":"E. Feron and F. Alegre. Control software analysis, part II: Closed-loop analysis. Technical report, arXiv:0812.1986, 2008."},{"key":"10.2168\/LMCS-8(1:1)2012_Feret","unstructured":"J. Feret. Numerical abstract domains for digital filters. InInternational workshop on Numerical and Symbolic Abstract Domains (NSAD 2005), 2005."},{"key":"10.2168\/LMCS-8(1:1)2012_Feron1","unstructured":"E Feron and Alegre F. Control software analysis, part I: Open-loop properties. Technical report, arXiv:0809.4812, 2008."},{"key":"10.2168\/LMCS-8(1:1)2012_ESOP07","doi-asserted-by":"crossref","unstructured":"S. Gaubert, E. Goubault, A. Taly, and S. Zennou. Static analysis by policy iteration on relational domains. InProceedings of the Sixteenth European Symposium Of Programming (ESOP'07), volume 4421 ofLNCS, pages 237-252. Springer, 2007.","DOI":"10.1007\/978-3-540-71316-6_17"},{"key":"10.2168\/LMCS-8(1:1)2012_GareyJohnson","unstructured":"M. R. Garey and D. Johnson.Computers and Intractability: A Guide to the Theory of NP-Completeness. W.H.Freeman & Co Ltd, 1979."},{"key":"10.2168\/LMCS-8(1:1)2012_GroetschelLovaszSchrijver1988","doi-asserted-by":"crossref","unstructured":"M. Gr\u00f6tschel, L. Lov\u00e1sz, and A. Schrijver.Geometric Algorithms and Combinatorial Optimization, volume 2 ofAlgorithms and Combinatorics. Springer, 1988.","DOI":"10.1007\/978-3-642-97881-4"},{"key":"10.2168\/LMCS-8(1:1)2012_FMICS07","doi-asserted-by":"crossref","unstructured":"E. Goubault, S. Putot, P. Baufreton, and J. Gassino. Static analysis of the accuracy in control systems: Principles and experiments. InFormal Methods for Industrial Critical System (FMICS 2007), volume 4916 ofLNCS, pages 3-20, 2008.","DOI":"10.1007\/978-3-540-79707-4_3"},{"key":"10.2168\/LMCS-8(1:1)2012_Seidl1","doi-asserted-by":"crossref","unstructured":"T. Gawlitza and H. Seidl. Precise fixpoint computation through strategy iteration. In R. De Nicola, editor,Programming Languages and Systems, 16th European Symposium on Programming, ESOP 2007, volume 4421 ofLNCS, pages 300-315. Springer, 2007.","DOI":"10.1007\/978-3-540-71316-6_21"},{"key":"10.2168\/LMCS-8(1:1)2012_Seidl2","unstructured":"T. Gawlitza and H. Seidl. Precise relational invariants through strategy iteration. In Jacques Duparc and Thomas A. Henzinger, editors,Computer Science Logic, 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007, Proceedings, volume 4646 ofLNCS, pages 23-40. Springer, 2007."},{"key":"10.2168\/LMCS-8(1:1)2012_DBLP:conf\/sas\/GawlitzaS10","doi-asserted-by":"crossref","unstructured":"T. M. Gawlitza and H. Seidl. Computing relaxed abstract semantics w.r.t. quadratic zones precisely. In Radhia Cousot and Matthieu Martel, editors,SAS, volume 6337 ofLecture Notes in Computer Science, pages 271-286. Springer, 2010.","DOI":"10.1007\/978-3-642-15769-1_17"},{"key":"10.2168\/LMCS-8(1:1)2012_ConvOpt","unstructured":"T. Gawlitza, H. Seidl, A. Adj\u00e9, S. Gaubert, and E. Goubault. Abstract interpretation meets convex optimization. To appear in Journal of symbolic computation, Special issue on invariant generation and advanced techniques for reasoning about loops."},{"key":"10.2168\/LMCS-8(1:1)2012_Hairer03","doi-asserted-by":"publisher","DOI":"10.1017\/S0962492902000144"},{"issue":"1","key":"10.2168\/LMCS-8(1:1)2012_jan-cha-kei-07","first-page":"180","volume":"46","author":"C. Jansson, D. Chaykin, and C. Keil","year":"2007","journal-title":"SIAM J. Numer. Anal."},{"key":"10.2168\/LMCS-8(1:1)2012_lurupa","unstructured":"C. Keil. Lurupa - rigorous error bounds in linear programming. InAlgebraic and Numerical Algorithms and Computer-assisted Proofs, 2005. http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2006\/445."},{"key":"10.2168\/LMCS-8(1:1)2012_Yalm","unstructured":"J. L\u00f6fberg. Yalmip : A toolbox for modeling and optimization in MATLAB. InProceedings of the CACSD Conference, Taipei, Taiwan, 2004. http:\/\/control.ee.ethz.ch\/ joloef\/yalmip.php."},{"key":"10.2168\/LMCS-8(1:1)2012_lasserre","doi-asserted-by":"publisher","DOI":"10.1137\/070693709"},{"key":"10.2168\/LMCS-8(1:1)2012_AGirard","doi-asserted-by":"crossref","unstructured":"C. Le Guernic and A. Girard. Reachability analysis of hybrid systems using support functions. In Ahmed Bouajjani and Oded Maler, editors,Computer Aided Verification, volume 5643 ofLecture Notes in Computer Science, pages 540-554. Springer Berlin \/ Heidelberg, 2009.","DOI":"10.1007\/978-3-642-02658-4_40"},{"key":"10.2168\/LMCS-8(1:1)2012_PhDMine","unstructured":"A. Min\u00e9.Weakly Relational Numerical Abstract Domains. PhD thesis, \u00c9cole Polytechnique, Palaiseau, France, December 2004. http:\/\/www.di.ens.fr\/ mine\/these\/these-color.pdf."},{"key":"10.2168\/LMCS-8(1:1)2012_Moreau","first-page":"109","volume":"49","author":"J. J. Moreau","year":"1970","journal-title":"Journal Math\u00e9matiques de Pures et Appliqu\u00e9es 1970"},{"key":"10.2168\/LMCS-8(1:1)2012_Muller","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2004.05.004"},{"key":"10.2168\/LMCS-8(1:1)2012_NestNemi","doi-asserted-by":"publisher","DOI":"10.1137\/1.9781611970791"},{"key":"10.2168\/LMCS-8(1:1)2012_parillo","doi-asserted-by":"publisher","DOI":"10.1007\/s10107-003-0387-5"},{"key":"10.2168\/LMCS-8(1:1)2012_RaP:97","doi-asserted-by":"crossref","unstructured":"P.M. Pardalos and M.V. Ramana. Semidefinite programming. InInterior Point Methods of Mathematical Programming, pages 369-398. Kluwer Academic Publishers, 1997.","DOI":"10.1007\/978-1-4613-3449-1_9"},{"key":"10.2168\/LMCS-8(1:1)2012_Kapur","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2006.03.003"},{"key":"10.2168\/LMCS-8(1:1)2012_Roc","unstructured":"R.T. Rockafellar.Convex Analysis. Princeston University Press, 1996."},{"key":"10.2168\/LMCS-8(1:1)2012_Rubinov","doi-asserted-by":"crossref","unstructured":"A. M. Rubinov.Abstract Convexity and Global optimization. Kluwer Academic Publishers, 2000.","DOI":"10.1007\/978-1-4757-3200-9"},{"key":"10.2168\/LMCS-8(1:1)2012_Sriram2","doi-asserted-by":"crossref","unstructured":"S. Sankaranarayanan, M. Colon, H. Sipma, and Z. Manna. Efficient strongly relational polyhedral analysis. In E. Allen Emerson and Kedar S. Namjoshi, editors,Verification, Model Checking, and Abstract Interpretation:7thInternational Conference, (VMCAI), volume 3855 ofLNCS, pages 111-125, Charleston, SC, January 2006. Springer.","DOI":"10.1007\/11609773_8"},{"issue":"6","key":"10.2168\/LMCS-8(1:1)2012_shor","first-page":"1","volume":"25","author":"N. Shor","year":"1987","journal-title":"Soviet J. of Computer and Systems Science"},{"key":"10.2168\/LMCS-8(1:1)2012_Singer","unstructured":"I. Singer.Abstract Convex Analysis. Wiley-Interscience Publication, 1997."},{"key":"10.2168\/LMCS-8(1:1)2012_Sriram1","doi-asserted-by":"crossref","unstructured":"S. Sankaranarayanan, H. B. Sipma, and Z. Manna. Scalable analysis of linear systems using mathematical programming. InSixth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'05), volume 3385 ofLNCS, pages 25-41, January 2005.","DOI":"10.1007\/978-3-540-30579-8_2"},{"key":"10.2168\/LMCS-8(1:1)2012_Sedu","doi-asserted-by":"publisher","DOI":"10.1080\/10556789908805766"},{"key":"10.2168\/LMCS-8(1:1)2012_BTN","doi-asserted-by":"publisher","DOI":"10.1137\/1.9780898718829"},{"key":"10.2168\/LMCS-8(1:1)2012_Vavasis90","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(90)90100-C"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/687\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/687\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T19:53:54Z","timestamp":1681242834000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/687"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,1,19]]},"references-count":42,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(1:1)2012","relation":{"references":[{"id-type":"doi","id":"10.1016\/j.ipl.2004.05.004","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"1111.5223","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1111.5223","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,1,19]]},"article-number":"687"}}