{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T04:19:52Z","timestamp":1748405992972,"version":"3.41.0"},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2015,4,1]],"date-time":"2015-04-01T00:00:00Z","timestamp":1427846400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2015,4]]},"DOI":"10.1007\/s10703-015-0230-7","type":"journal-article","created":{"date-parts":[[2015,5,2]],"date-time":"2015-05-02T12:31:58Z","timestamp":1430569918000},"page":"163-196","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Practical policy iterations"],"prefix":"10.1007","volume":"46","author":[{"given":"Pierre","family":"Roux","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0513-6076","authenticated-orcid":false,"given":"Pierre-Lo\u00efc","family":"Garoche","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,5,3]]},"reference":[{"key":"230_CR1","doi-asserted-by":"crossref","unstructured":"Adj\u00e9 A, Gaubert S, Goubault E (2010) Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis. In: ESOP, pp 23\u201342","DOI":"10.1007\/978-3-642-11957-6_3"},{"key":"230_CR2","unstructured":"Alegre F, F\u00e9ron E, Pande S (2009) Using ellipsoidal domains to analyze control systems software. arXiv:0909.1977"},{"key":"230_CR3","doi-asserted-by":"crossref","unstructured":"Boldo S, Melquiond G (2011) Flocq: a unified library for proving floating-point algorithms in Coq. In: Proceedings of the 20th IEEE symposium on computer arithmetic. T\u00fcbingen, pp 243\u2013252","DOI":"10.1109\/ARITH.2011.40"},{"issue":"12","key":"230_CR4","doi-asserted-by":"crossref","first-page":"1479","DOI":"10.1016\/j.jsc.2011.12.050","volume":"47","author":"O Bouissou","year":"2012","unstructured":"Bouissou O, Seladji Y, Chapoutot A (2012) Acceleration of the abstract fixpoint computation in numerical program analysis. J Symb Comput 47(12):1479\u20131511","journal-title":"J Symb Comput"},{"key":"230_CR5","doi-asserted-by":"crossref","DOI":"10.1137\/1.9781611970777","volume-title":"Linear matrix inequalities in system and control theory, volume 15 of SIAM","author":"S Boyd","year":"1994","unstructured":"Boyd S, El Ghaoui L, F\u00e9ron E, Balakrishnan V (1994) Linear matrix inequalities in system and control theory, volume 15 of SIAM. SIAM, Philadelphia"},{"key":"230_CR6","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511804441","volume-title":"Convex optimization","author":"S Boyd","year":"2004","unstructured":"Boyd S, Vandenberghe L (2004) Convex optimization. Cambridge University Press, Cambridge"},{"key":"230_CR7","doi-asserted-by":"crossref","unstructured":"Champion A, Delmas R, Dierkes M, Garoche P-L, Jobredeaux R, Roux P (2013) Formal methods for the analysis of critical control systems models: combining non-linear and linear analyses. In: Charles P, Michael D, (eds), Formal methods for industrial critical systems\u201418th international workshop, FMICS 2013, Madrid, Spain, September 23\u201324, 2013. Proceedings, volume 8187 of Lecture Notes in Computer Science, pp 1\u201316. Springer","DOI":"10.1007\/978-3-642-41010-9_1"},{"key":"230_CR8","doi-asserted-by":"crossref","unstructured":"Costan A, Gaubert S, Goubault E, Martel M, Putot S (2005) A policy iteration algorithm for computing fixed points in static analysis of programs. In: CAV, pp 462\u2013475","DOI":"10.1007\/11513988_46"},{"key":"230_CR9","doi-asserted-by":"crossref","unstructured":"Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp 238\u2013252","DOI":"10.1145\/512950.512973"},{"key":"230_CR10","doi-asserted-by":"crossref","unstructured":"Cousot P, Cousot R (1979) Systematic design of program analysis frameworks. In: POPL, pp 269\u2013282","DOI":"10.1145\/567752.567778"},{"issue":"4","key":"230_CR11","doi-asserted-by":"crossref","first-page":"511","DOI":"10.1093\/logcom\/2.4.511","volume":"2","author":"P Cousot","year":"1992","unstructured":"Cousot P, Cousot R (1992) Abstract interpretation frameworks. J Log Comput 2(4):511\u2013547","journal-title":"J Log Comput"},{"key":"230_CR12","doi-asserted-by":"crossref","unstructured":"Cousot P, Halbwachs N (1978) Automatic discovery of linear restraints among variables of a program. In: POPL, pp 84\u201396","DOI":"10.1145\/512760.512770"},{"issue":"2","key":"230_CR13","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.entcs.2010.09.014","volume":"267","author":"P Feautrier","year":"2010","unstructured":"Feautrier P, Gonnord L (2010) Accelerated invariant generation for c programs with aspic and c2fsm. Electron Notes Theor Comput Sci 267(2):3\u201313","journal-title":"Electron Notes Theor Comput Sci"},{"key":"230_CR14","doi-asserted-by":"crossref","unstructured":"Feret J (2004) Static analysis of digital filters. In: ESOP, number 2986 in LNCS. Springer","DOI":"10.1007\/978-3-540-24725-8_4"},{"key":"230_CR15","unstructured":"Feret J (2005) Numerical abstract domains for digital filters. In: International workshop on Numerical and Symbolic Abstract Domains (NSAD)"},{"issue":"6","key":"230_CR16","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1109\/MCS.2010.938196","volume":"30","author":"E F\u00e9ron","year":"2010","unstructured":"F\u00e9ron E (2010) From control systems to control software. IEEE Control Syst 30(6):50\u201371","journal-title":"IEEE Control Syst"},{"key":"230_CR17","doi-asserted-by":"crossref","unstructured":"Gaubert S, Goubault E, Taly A, Zennou S (2007) Static analysis by policy iteration on relational domains. In: ESOP, pp 237\u2013252","DOI":"10.1007\/978-3-540-71316-6_17"},{"key":"230_CR18","doi-asserted-by":"crossref","unstructured":"Gawlitza T, Seidl H (2007) Precise fixpoint computation through strategy iteration. In: ESOP, pp 300\u2013315","DOI":"10.1007\/978-3-540-71316-6_21"},{"key":"230_CR19","unstructured":"Gawlitza TM, Seidl H (2010) Computing relaxed abstract semantics w.r.t. quadratic zones precisely. In: SAS, pp 271\u2013286"},{"issue":"12","key":"230_CR20","doi-asserted-by":"crossref","first-page":"1416","DOI":"10.1016\/j.jsc.2011.12.048","volume":"47","author":"TM Gawlitza","year":"2012","unstructured":"Gawlitza TM, Seidl H, Adj\u00e9 A, Gaubert S, Goubault E (2012) Abstract interpretation meets convex optimization. J Symb Comput 47(12):1416\u20131446","journal-title":"J Symb Comput"},{"key":"230_CR21","doi-asserted-by":"crossref","unstructured":"Ghorbal K, Goubault E, Putot S (2009) The zonotope abstract domain taylor1+. In: CAV, pp 627\u2013633","DOI":"10.1007\/978-3-642-02658-4_47"},{"key":"230_CR22","doi-asserted-by":"crossref","unstructured":"Gopan D, Reps TW (2006) Lookahead widening. In: CAV, pp 452\u2013466","DOI":"10.1007\/11817963_41"},{"key":"230_CR23","doi-asserted-by":"crossref","unstructured":"Goubault E, Putot S (2011) Static analysis of finite precision computations. In: VMCAI, pp 232\u2013247","DOI":"10.1007\/978-3-642-18275-4_17"},{"key":"230_CR24","doi-asserted-by":"crossref","DOI":"10.1515\/9781400841042","volume-title":"Nonlinear dynamical systems and control: a lyapunov-based approach","author":"WM Haddad","year":"2008","unstructured":"Haddad WM, Chellaboina VS (2008) Nonlinear dynamical systems and control: a lyapunov-based approach. Princeton University Press, Princeton"},{"key":"230_CR25","doi-asserted-by":"crossref","unstructured":"Halbwachs N, Henry J (2012) When the decreasing sequence fails. In: SAS, pp 198\u2013213","DOI":"10.1007\/978-3-642-33125-1_15"},{"issue":"2","key":"230_CR26","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1023\/A:1008678014487","volume":"11","author":"Nicolas Halbwachs","year":"1997","unstructured":"Halbwachs Nicolas, Proy Yann-Erick, Roumanoff Patrick (1997) Verification of real-time systems using linear relation analysis. Formal Methods in System Design 11(2):157\u2013185","journal-title":"Formal Methods in System Design"},{"key":"230_CR27","volume-title":"Accuracy and stability of numerical algorithms","author":"NJ Higham","year":"1996","unstructured":"Higham NJ (1996) Accuracy and stability of numerical algorithms. Society for Industrial and Applied Mathematics, Philadelphia"},{"key":"230_CR28","unstructured":"IEEE Computer Society (2008) IEEE standard for floating-point arithmetic. In: IEEE Standard 754\u20132008"},{"key":"230_CR29","volume-title":"Probl\u00e8me g\u00e9n\u00e9ral de la stabilit\u00e9 du mouvement. Annals of Mathematics Studies 17","author":"AM Lyapunov","year":"1947","unstructured":"Lyapunov AM (1947) Probl\u00e8me g\u00e9n\u00e9ral de la stabilit\u00e9 du mouvement. Annals of Mathematics Studies 17. Princeton University Press, Princeton"},{"key":"230_CR30","doi-asserted-by":"crossref","unstructured":"Min\u00e9 A (2001) The octagon abstract domain. In: AST 2001 in WCRE 2001, IEEE, pp 310\u2013319. IEEE CS Press","DOI":"10.1109\/WCRE.2001.957836"},{"key":"230_CR31","doi-asserted-by":"crossref","unstructured":"Min\u00e9 A (2004) Relational abstract domains for the detection of floating-point run-time errors. In: ESOP, volume 2986 of LNCS, pp 3\u201317. Springer, http:\/\/www.di.ens.fr\/~mine\/publi\/article-mine-esop04.pdf","DOI":"10.1007\/978-3-540-24725-8_2"},{"key":"230_CR32","doi-asserted-by":"crossref","unstructured":"Monniaux D (2005) Compositional analysis of floating-point linear numerical filters. In: CAV, pp 199\u2013212","DOI":"10.1007\/11513988_21"},{"key":"230_CR33","doi-asserted-by":"crossref","unstructured":"Roozbehani M, F\u00e9ron E, Megretski A (2005) Modeling, optimization and computation for software verification. In: HSCC, pp 606\u2013622","DOI":"10.1007\/978-3-540-31954-2_39"},{"key":"230_CR34","unstructured":"Roux P (2013) Static analysis of control command systems: synthetizing non linear invariants. PhD thesis, Institut Sup\u00e9rieur de l\u2019A\u00e9ronautique et de l\u2019Espace"},{"key":"230_CR35","doi-asserted-by":"crossref","unstructured":"Roux P, Garoche P-L (2013) Integrating policy iterations in abstract interpreters. In: Dang Van Hung and Mizuhito Ogawa, (eds), Automated technology for verification and analysis\u201411th international symposium, ATVA 2013, Hanoi, Vietnam, October 15\u201318, 2013. Proceedings, volume 8172 of Lecture Notes in Computer Science, pp 240\u2013254. Springer","DOI":"10.1007\/978-3-319-02444-8_18"},{"key":"230_CR36","doi-asserted-by":"crossref","unstructured":"Roux P, Garoche P-L (2014) Computing quadratic invariants with min- and max-policy iterations: a practical comparison. In: Jones CB, Pihlajasaari P, Sun J (eds), FM 2014: formal methods\u201419th international symposium, Singapore, May 12\u201316, 2014. Proceedings, volume 8442 of Lecture Notes in Computer Science, pp 563\u2013578. Springer","DOI":"10.1007\/978-3-319-06410-9_38"},{"key":"230_CR37","doi-asserted-by":"crossref","unstructured":"Roux P, Jobredeaux R, Garoche P-L, F\u00e9ron E (2012) A generic ellipsoid abstract domain for linear time invariant systems. In: HSCC, pp 105\u2013114","DOI":"10.1145\/2185632.2185651"},{"key":"230_CR38","doi-asserted-by":"crossref","first-page":"433","DOI":"10.1007\/s10543-006-0056-1","volume":"46","author":"SM Rump","year":"2006","unstructured":"Rump SM (2006) Verification of positive definiteness. BIT Numer Math 46:433\u2013452","journal-title":"BIT Numer Math"},{"key":"230_CR39","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1017\/S096249291000005X","volume":"19","author":"SM Rump","year":"2010","unstructured":"Rump SM (2010) Verification methods: Rigorous results using floating-point arithmetic. Acta Numer 19:287\u2013449","journal-title":"Acta Numer"},{"key":"230_CR40","doi-asserted-by":"crossref","unstructured":"Schrammel P, Jeannet B (2011) Logico-numerical abstract acceleration and application to the verification of data-flow programs. In: SAS, pp 233\u2013248","DOI":"10.1007\/978-3-642-23702-7_19"},{"key":"230_CR41","first-page":"155","volume":"7871","author":"Y Seladji","year":"2013","unstructured":"Seladji Y, Bouissou O (2013) Numerical abstract domain using support functions. NFM 7871:155\u2013169","journal-title":"NFM"},{"key":"230_CR42","unstructured":"The Coq Development Team (2013) The Coq proof assistant reference manual, 2012. Version 8.4. Springer, Heidelberg"},{"issue":"1","key":"230_CR43","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1137\/1038003","volume":"38","author":"L Vandenberghe","year":"1996","unstructured":"Vandenberghe L, Boyd S (1996) Semidefinite programming. SIAM Rev 38(1):49\u201395","journal-title":"SIAM Rev"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-015-0230-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-015-0230-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-015-0230-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,27]],"date-time":"2025-05-27T19:42:06Z","timestamp":1748374926000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-015-0230-7"}},"subtitle":["A practical use of policy iterations for static analysis: the quadratic case"],"short-title":[],"issued":{"date-parts":[[2015,4]]},"references-count":43,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2015,4]]}},"alternative-id":["230"],"URL":"https:\/\/doi.org\/10.1007\/s10703-015-0230-7","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2015,4]]}}}