{"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":1775868493641,"version":"3.50.1"},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2013,9,22]],"date-time":"2013-09-22T00:00:00Z","timestamp":1379808000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2014,4]]},"DOI":"10.1007\/s10703-013-0190-8","type":"journal-article","created":{"date-parts":[[2013,9,21]],"date-time":"2013-09-21T08:13:50Z","timestamp":1379751230000},"page":"101-148","source":"Crossref","is-referenced-by-count":2,"title":["Numerical invariants through convex relaxation and max-strategy iteration"],"prefix":"10.1007","volume":"44","author":[{"given":"Thomas Martin","family":"Gawlitza","sequence":"first","affiliation":[]},{"given":"Helmut","family":"Seidl","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2013,9,22]]},"reference":[{"key":"190_CR1","series-title":"Lecture notes in computer science","isbn-type":"print","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1007\/978-3-642-11957-6_3","volume-title":"ESOP","author":"A Adj\u00e9","year":"2010","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: Gordon AD (ed) ESOP. Lecture notes in computer science, vol 6012. Springer, Berlin, pp\u00a023\u201342. ISBN 978-3-642-11956-9","ISBN":"https:\/\/id.crossref.org\/isbn\/9783642119569"},{"key":"190_CR2","unstructured":"Alegre F, Feron E, Pande S (2009) Using ellipsoidal domains to analyze control systems software. arXiv:0909.1977"},{"key":"190_CR3","isbn-type":"print","doi-asserted-by":"crossref","first-page":"178","DOI":"10.1145\/41625.41641","volume-title":"POPL","author":"P Caspi","year":"1987","unstructured":"Caspi P, Pilaud D, Halbwachs N, Plaice J (1987) Lustre: a declarative language for programming synchronous systems. In: POPL. ACM, New York, pp\u00a0178\u2013188. ISBN 0-89791-215-2","ISBN":"https:\/\/id.crossref.org\/isbn\/0897912152"},{"key":"190_CR4","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"462","DOI":"10.1007\/11513988_46","volume-title":"Computer aided verification, 17th int conf (CAV)","author":"A Costan","year":"2005","unstructured":"Costan A, Gaubert S, Goubault E, Martel M, Putot S (2005) A policy iteration algorithm\u00a0for computing fixed points in static analysis of programs. In: Computer aided verification, 17th int conf (CAV). Lecture notes in computer science, vol 3576. Springer, Berlin, pp\u00a0462\u2013475"},{"key":"190_CR5","first-page":"106","volume-title":"Second int symp on programming","author":"P Cousot","year":"1976","unstructured":"Cousot P, Cousot R (1976) Static determination of dynamic properties of programs. In: Second int symp on programming. Dunod, Paris, pp\u00a0106\u2013130"},{"key":"190_CR6","first-page":"238","volume-title":"POPL","author":"P Cousot","year":"1977","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\u00a0238\u2013252"},{"key":"190_CR7","series-title":"Lecture notes in computer science","isbn-type":"print","doi-asserted-by":"crossref","first-page":"34","DOI":"10.1007\/978-3-642-25318-8_6","volume-title":"APLAS","author":"T Dang","year":"2011","unstructured":"Dang T, Gawlitza TM (2011) Template-based unbounded time verification of affine hybrid automata. In: Yang H (ed) APLAS. Lecture notes in computer science, vol 7078. Springer, Berlin, pp\u00a034\u201349. ISBN 978-3-642-25317-1","ISBN":"https:\/\/id.crossref.org\/isbn\/9783642253171"},{"key":"190_CR8","series-title":"Lecture notes in computer science","isbn-type":"print","doi-asserted-by":"crossref","first-page":"473","DOI":"10.1007\/978-3-642-24372-1_36","volume-title":"ATVA","author":"T Dang","year":"2011","unstructured":"Dang T, Gawlitza TM (2011) Discretizing affine hybrid automata with uncertainty. In: Bultan T, Hsiung P-A (eds) ATVA. Lecture notes in computer science, vol 6996. Springer, Berlin, pp\u00a0473\u2013481. ISBN 978-3-642-24371-4","ISBN":"https:\/\/id.crossref.org\/isbn\/9783642243714"},{"key":"190_CR9","series-title":"Lecture notes in computer science","isbn-type":"print","doi-asserted-by":"crossref","first-page":"551","DOI":"10.1007\/978-3-642-14162-1_46","volume-title":"ICALP (2)","author":"J Fearnley","year":"2010","unstructured":"Fearnley J (2010) Exponential lower bounds for policy iteration. In: Abramsky S, Gavoille C, Kirchner C, Meyer auf der Heide F, Spirakis PG (eds) ICALP (2). Lecture notes in computer science, vol 6199. Springer, Berlin, pp\u00a0551\u2013562. ISBN 978-3-642-14161-4","ISBN":"https:\/\/id.crossref.org\/isbn\/9783642141614"},{"key":"190_CR10","series-title":"Lecture notes in computer science","isbn-type":"print","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1007\/978-3-540-74915-8_6","volume-title":"CSL","author":"T Gawlitza","year":"2007","unstructured":"Gawlitza T, Seidl H (2007) Precise relational invariants through strategy iteration. In: Duparc J, Henzinger TA (eds) CSL. Lecture notes in computer science, vol 4646. Springer, Berlin, pp\u00a023\u201340. ISBN 978-3-540-74914-1","ISBN":"https:\/\/id.crossref.org\/isbn\/9783540749141"},{"key":"190_CR11","series-title":"Lecture notes in computer science","isbn-type":"print","doi-asserted-by":"crossref","first-page":"300","DOI":"10.1007\/978-3-540-71316-6_21","volume-title":"ESOP","author":"T Gawlitza","year":"2007","unstructured":"Gawlitza T, Seidl H (2007) Precise fixpoint computation through strategy iteration. In: Nicola RD (ed) ESOP. Lecture notes in computer science, vol 4421. Springer, Berlin, pp\u00a0300\u2013315. ISBN 978-3-540-71314-2","ISBN":"https:\/\/id.crossref.org\/isbn\/9783540713142"},{"key":"190_CR12","series-title":"Lecture notes in computer science","isbn-type":"print","doi-asserted-by":"crossref","first-page":"342","DOI":"10.1007\/978-3-540-68237-0_24","volume-title":"FM","author":"T Gawlitza","year":"2008","unstructured":"Gawlitza T, Seidl H (2008) Precise interval analysis vs. parity games. In: Cu\u00e9llar J, Maibaum TSE, Sere K (eds) FM. Lecture notes in computer science, vol 5014. Springer, Berlin, pp\u00a0342\u2013357. ISBN 978-3-540-68235-6","ISBN":"https:\/\/id.crossref.org\/isbn\/9783540682356"},{"key":"190_CR13","series-title":"Lecture notes in computer science","isbn-type":"print","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1007\/978-3-642-15769-1_17","volume-title":"SAS","author":"TM Gawlitza","year":"2010","unstructured":"Gawlitza TM, Seidl H (2010) Computing relaxed abstract semantics w.r.t. quadratic zones precisely. In: Cousot R, Martel M (eds) SAS. Lecture notes in computer science, vol 6337. Springer, Berlin, pp\u00a0271\u2013286. ISBN 978-3-642-15768-4","ISBN":"https:\/\/id.crossref.org\/isbn\/9783642157684"},{"issue":"3","key":"190_CR14","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1145\/1961204.1961207","volume":"33","author":"TM Gawlitza","year":"2011","unstructured":"Gawlitza TM, Seidl H (2011) Solving systems of rational equations through strategy iteration. ACM Trans Program Lang Syst 33(3):11","journal-title":"ACM Trans Program Lang Syst"},{"key":"190_CR15","volume-title":"WING-JSC","author":"TM Gawlitza","year":"2011","unstructured":"Gawlitza TM, Seidl H, Adj\u00e9 A, Gaubert S, Goubault \u00c9 (2011) Abstract interpretation meets convex optimization. In: WING-JSC"},{"key":"190_CR16","series-title":"Lecture notes in computer science","isbn-type":"print","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1007\/978-3-540-31954-2_19","volume-title":"HSCC","author":"A Girard","year":"2005","unstructured":"Girard A (2005) Reachability of uncertain linear systems using zonotopes. In: Morari M, Thiele L (eds) HSCC. Lecture notes in computer science, vol 3414. Springer, Berlin, pp\u00a0291\u2013305. ISBN 3-540-25108-1","ISBN":"https:\/\/id.crossref.org\/isbn\/3540251081"},{"key":"190_CR17","first-page":"3","volume-title":"MEMOCODE","author":"N Halbwachs","year":"2005","unstructured":"Halbwachs N (2005) A synchronous language at work: the story of lustre. In: MEMOCODE. IEEE Press, New York, pp\u00a03\u201311"},{"issue":"9","key":"190_CR18","doi-asserted-by":"crossref","first-page":"785","DOI":"10.1109\/32.159839","volume":"18","author":"N Halbwachs","year":"1992","unstructured":"Halbwachs N, Lagnier F, Ratel C (1992) Programming and verifying real-time systems by means of the synchronous data-flow language lustre. IEEE Trans Softw Eng 18(9):785\u2013793","journal-title":"IEEE Trans Softw Eng"},{"key":"190_CR19","first-page":"14","volume-title":"IEEE real-time systems symposium","author":"KG Larsen","year":"1997","unstructured":"Larsen KG, Larsson F, Pettersson P, Yi W (1997) Efficient verification of real-time systems: compact data structure and state-space reduction. In: IEEE real-time systems symposium. IEEE Comput Soc, Los Alamitos, pp\u00a014\u201324"},{"key":"190_CR20","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1016\/j.entcs.2012.09.008","volume":"287","author":"D Mass\u00e9","year":"2012","unstructured":"Mass\u00e9 D (2012) Proving termination by policy iteration. Electron Notes Theor Comput Sci 287:77\u201388. doi: 10.1016\/j.entcs.2012.09.008","journal-title":"Electron Notes Theor Comput Sci"},{"key":"190_CR21","series-title":"Lecture notes in computer science","isbn-type":"print","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1007\/3-540-44978-7_10","volume-title":"PADO","author":"A Min\u00e9","year":"2001","unstructured":"Min\u00e9 A (2001) A new numerical abstract domain based on difference-bound matrices. In: Danvy O, Filinski A (eds) PADO. Lecture notes in computer science, vol 2053. Springer, Berlin, pp\u00a0155\u2013172. ISBN 3-540-42068-1","ISBN":"https:\/\/id.crossref.org\/isbn\/3540420681"},{"key":"190_CR22","first-page":"310","volume-title":"WCRE","author":"A Min\u00e9","year":"2001","unstructured":"Min\u00e9 A (2001) The octagon abstract domain. In: WCRE, p 310"},{"key":"190_CR23","unstructured":"Nemirovski A (2005) Modern convex optimization. Department ISYE, Georgia Institute of Technology"},{"key":"190_CR24","unstructured":"Roux P, Garoche P-L (2012) Policy iterations as traditional abstract domains"},{"key":"190_CR25","isbn-type":"print","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1145\/2185632.2185651","volume-title":"HSCC","author":"P Roux","year":"2012","unstructured":"Roux P, Jobredeaux R, Garoche P-L, Feron E (2012) A generic ellipsoid abstract domain for linear time invariant systems. In: Dang T, Mitchell IM (eds) HSCC. ACM, New York, pp\u00a0105\u2013114. ISBN 978-1-4503-1220-2","ISBN":"https:\/\/id.crossref.org\/isbn\/9781450312202"},{"key":"190_CR26","series-title":"Lecture notes in computer science","isbn-type":"print","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1007\/978-3-540-30579-8_2","volume-title":"VMCAI","author":"S Sankaranarayanan","year":"2005","unstructured":"Sankaranarayanan S, Sipma HB, Manna Z (2005) Scalable analysis of linear systems using mathematical programming. In: Cousot R (ed) VMCAI. Lecture notes in computer science, vol 3385. Springer, Berlin, pp\u00a025\u201341. ISBN 3-540-24297-X","ISBN":"https:\/\/id.crossref.org\/isbn\/354024297X"},{"key":"190_CR27","series-title":"Lecture notes in computer science","isbn-type":"print","doi-asserted-by":"crossref","first-page":"654","DOI":"10.1007\/978-3-540-78929-1_57","volume-title":"HSCC","author":"S Sankaranarayanan","year":"2008","unstructured":"Sankaranarayanan S, Dang T, Ivancic F (2008) A policy iteration technique for time elapse over template polyhedra. In: Egerstedt M, Mishra B (eds) HSCC. Lecture notes in computer science, vol 4981. Springer, Berlin, pp\u00a0654\u2013657. ISBN 978-3-540-78928-4","ISBN":"https:\/\/id.crossref.org\/isbn\/9783540789284"},{"key":"190_CR28","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A Tarski","year":"1955","unstructured":"Tarski A (1955) A lattice-theoretical fixpoint theorem and its applications. Pac J Math 5:285\u2013309","journal-title":"Pac J Math"},{"key":"190_CR29","doi-asserted-by":"crossref","first-page":"515","DOI":"10.1017\/S0962492901000071","volume":"10","author":"MJ Todd","year":"2001","unstructured":"Todd MJ (2001) Semidefinite optimization. Acta Numer 10:515\u2013560","journal-title":"Acta Numer"},{"key":"190_CR30","series-title":"Lecture notes in computer science","isbn-type":"print","first-page":"114","volume-title":"European educational forum: school on embedded systems","author":"S Yovine","year":"1996","unstructured":"Yovine S (1996) Model checking timed automata. In: Rozenberg G, Vaandrager FW (eds) European educational forum: school on embedded systems. Lecture notes in computer science, vol 1494. Springer, Berlin, pp\u00a0114\u2013152. ISBN 3-540-65193-4","ISBN":"https:\/\/id.crossref.org\/isbn\/3540651934"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-013-0190-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-013-0190-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-013-0190-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,24]],"date-time":"2019-07-24T11:30:10Z","timestamp":1563967810000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-013-0190-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,9,22]]},"references-count":30,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2014,4]]}},"alternative-id":["190"],"URL":"https:\/\/doi.org\/10.1007\/s10703-013-0190-8","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,9,22]]}}}