{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:15:49Z","timestamp":1763468149778},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319024431"},{"type":"electronic","value":"9783319024448"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-319-02444-8_18","type":"book-chapter","created":{"date-parts":[[2013,8,29]],"date-time":"2013-08-29T01:11:21Z","timestamp":1377738681000},"page":"240-254","source":"Crossref","is-referenced-by-count":7,"title":["Integrating Policy Iterations in Abstract Interpreters"],"prefix":"10.1007","author":[{"given":"Pierre","family":"Roux","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pierre-Lo\u00efc","family":"Garoche","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"18_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-11957-6_3","volume-title":"Programming Languages and Systems","author":"A. Adj\u00e9","year":"2010","unstructured":"Adj\u00e9, A., Gaubert, S., Goubault, E.: Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol.\u00a06012, pp. 23\u201342. Springer, Heidelberg (2010)"},{"issue":"1-4","key":"18_CR2","doi-asserted-by":"publisher","first-page":"613","DOI":"10.1080\/10556789908805765","volume":"11","author":"Brian Borchers","year":"1999","unstructured":"Borchers, B.: Csdp, a c library for semidefinite programming. Optimization Methods and Software\u00a011(1-4) (1999)","journal-title":"Optimization Methods and Software"},{"issue":"12","key":"18_CR3","doi-asserted-by":"publisher","first-page":"1479","DOI":"10.1016\/j.jsc.2011.12.050","volume":"47","author":"Olivier Bouissou","year":"2012","unstructured":"Bouissou, O., Seladji, Y., Chapoutot, A.: Acceleration of the abstract fixpoint computation in numerical program analysis. J. Symb. Comput.\u00a047(12) (2012)","journal-title":"Journal of Symbolic Computation"},{"key":"18_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/BFb0039704","volume-title":"Formal Methods in Programming and Their Applications","author":"F. Bourdoncle","year":"1993","unstructured":"Bourdoncle, F.: Efficient chaotic iteration strategies with widenings. In: Pottosin, I.V., Bjorner, D., Broy, M. (eds.) FMP&TA 1993. LNCS, vol.\u00a0735, pp. 128\u2013141. Springer, Heidelberg (1993)"},{"key":"18_CR5","doi-asserted-by":"publisher","DOI":"10.1137\/1.9781611970777","volume-title":"Linear Matrix Inequalities in System and Control Theory","author":"S. Boyd","year":"1994","unstructured":"Boyd, S., El Ghaoui, L., F\u00e9ron, \u00c9., Balakrishnan, V.: Linear Matrix Inequalities in System and Control Theory, vol.\u00a015. SIAM, Philadelphia (1994)"},{"key":"18_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"462","DOI":"10.1007\/11513988_46","volume-title":"Computer Aided Verification","author":"A. Costan","year":"2005","unstructured":"Costan, A., Gaubert, S., Goubault, E., Martel, M., Putot, S.: A policy iteration algorithm for computing fixed points in static analysis of programs. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 462\u2013475. Springer, Heidelberg (2005)"},{"key":"18_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-30579-8_1","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P. Cousot","year":"2005","unstructured":"Cousot, P.: Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 1\u201324. Springer, Heidelberg (2005)"},{"key":"18_CR8","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL (1977)","DOI":"10.1145\/512950.512973"},{"issue":"3","key":"18_CR9","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/s10703-009-0089-6","volume":"35","author":"P. Cousot","year":"2009","unstructured":"Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Rival, X.: Why does astr\u00e9e scale up? Formal Methods in System Design\u00a035(3), 229\u2013264 (2009)","journal-title":"Formal Methods in System Design"},{"key":"18_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/978-3-540-77505-8_23","volume-title":"Advances in Computer Science - ASIAN 2006. Secure Software and Related Issues","author":"P. Cousot","year":"2008","unstructured":"Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: Combination of abstractions in the Astr\u00e9e static analyzer. In: Okada, M., Satoh, I. (eds.) ASIAN 2006. LNCS, vol.\u00a04435, pp. 272\u2013300. Springer, Heidelberg (2008)"},{"issue":"2","key":"18_CR11","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2010.09.014","volume":"267","author":"Paul Feautrier","year":"2010","unstructured":"Feautrier, P., Gonnord, L.: Accelerated invariant generation for c programs with aspic and c2fsm. Electr. Notes Theor. Comput. Sci.\u00a0267(2) (2010)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"18_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-540-24725-8_4","volume-title":"Programming Languages and Systems","author":"J. Feret","year":"2004","unstructured":"Feret, J.: Static analysis of digital filters. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol.\u00a02986, pp. 33\u201348. Springer, Heidelberg (2004)"},{"key":"18_CR13","unstructured":"Feret, J.: Numerical abstract domains for digital filters. In: International Workshop on Numerical and Symbolic Abstract Domains, NSAD (2005)"},{"key":"18_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-540-71316-6_17","volume-title":"Programming Languages and Systems","author":"S. Gaubert","year":"2007","unstructured":"Gaubert, S., Goubault, E., Taly, A., Zennou, S.: Static analysis by policy iteration on relational domains. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol.\u00a04421, pp. 237\u2013252. Springer, Heidelberg (2007)"},{"key":"18_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1007\/978-3-540-71316-6_21","volume-title":"Programming Languages and Systems","author":"T. Gawlitza","year":"2007","unstructured":"Gawlitza, T., Seidl, H.: Precise fixpoint computation through strategy iteration. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol.\u00a04421, pp. 300\u2013315. Springer, Heidelberg (2007)"},{"key":"18_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-540-74915-8_6","volume-title":"Computer Science Logic","author":"T. Gawlitza","year":"2007","unstructured":"Gawlitza, T., Seidl, H.: Precise relational invariants through strategy iteration. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol.\u00a04646, pp. 23\u201340. Springer, Heidelberg (2007)"},{"key":"18_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/978-3-642-19718-5_13","volume-title":"Programming Languages and Systems","author":"T.M. Gawlitza","year":"2011","unstructured":"Gawlitza, T.M., Monniaux, D.: Improving strategies via SMT solving. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol.\u00a06602, pp. 236\u2013255. Springer, Heidelberg (2011)"},{"key":"18_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/978-3-642-15769-1_17","volume-title":"Static Analysis","author":"T.M. Gawlitza","year":"2010","unstructured":"Gawlitza, T.M., Seidl, H.: Computing relaxed abstract semantics w.r.t. Quadratic zones precisely. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol.\u00a06337, pp. 271\u2013286. Springer, Heidelberg (2010)"},{"issue":"12","key":"18_CR19","doi-asserted-by":"publisher","first-page":"1416","DOI":"10.1016\/j.jsc.2011.12.048","volume":"47","author":"Thomas Martin Gawlitza","year":"2012","unstructured":"Gawlitza, T.M., Seidl, H., Adj\u00e9, A., Gaubert, S., Goubault, E.: Abstract interpretation meets convex optimization. J. Symb. Comput.\u00a047(12) (2012)","journal-title":"Journal of Symbolic Computation"},{"key":"18_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"627","DOI":"10.1007\/978-3-642-02658-4_47","volume-title":"Computer Aided Verification","author":"K. Ghorbal","year":"2009","unstructured":"Ghorbal, K., Goubault, E., Putot, S.: The zonotope abstract domain taylor1+. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 627\u2013633. Springer, Heidelberg (2009)"},{"key":"18_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1007\/11817963_41","volume-title":"Computer Aided Verification","author":"D. Gopan","year":"2006","unstructured":"Gopan, D., Reps, T.: Lookahead widening. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 452\u2013466. Springer, Heidelberg (2006)"},{"key":"18_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1007\/978-3-642-33125-1_15","volume-title":"Static Analysis","author":"N. Halbwachs","year":"2012","unstructured":"Halbwachs, N., Henry, J.: When the decreasing sequence fails. In: Min\u00e9, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol.\u00a07460, pp. 198\u2013213. Springer, Heidelberg (2012)"},{"key":"18_CR23","doi-asserted-by":"crossref","unstructured":"Jeannet, B.: Some experience on the software engineering of abstract interpretation tools. Electr. Notes Theor. Comput. Sci. (2) (2010)","DOI":"10.1016\/j.entcs.2010.09.016"},{"key":"18_CR24","unstructured":"Min\u00e9, A.: The octagon abstract domain. In: AST 2001 in WCRE 2001. IEEE (October 2001)"},{"key":"18_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/11513988_21","volume-title":"Computer Aided Verification","author":"D. Monniaux","year":"2005","unstructured":"Monniaux, D.: Compositional analysis of floating-point linear numerical filters. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 199\u2013212. Springer, Heidelberg (2005)"},{"key":"18_CR26","doi-asserted-by":"crossref","unstructured":"Roux, P., Jobredeaux, R., Garoche, P.-L., F\u00e9ron, \u00c9.: A generic ellipsoid abstract domain for linear time invariant systems. In: HSCC. ACM (2012)","DOI":"10.1145\/2185632.2185651"},{"issue":"2","key":"18_CR27","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1007\/s10543-006-0056-1","volume":"46","author":"S.M. Rump","year":"2006","unstructured":"Rump, S.M.: Verification of positive definiteness. BIT Numerical Mathematics\u00a046 (2006)","journal-title":"BIT Numerical Mathematics"},{"key":"18_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1007\/978-3-642-23702-7_19","volume-title":"SAS 2011","author":"P. Schrammel","year":"2011","unstructured":"Schrammel, P., Jeannet, B.: Logico-numerical abstract acceleration and application to the verification of data-flow programs. In: Yahav, E. (ed.) SAS 2011. LNCS, vol.\u00a06887, pp. 233\u2013248. Springer, Heidelberg (2011)"},{"key":"18_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/978-3-642-38088-4_11","volume-title":"NASA Formal Methods","author":"Y. Seladji","year":"2013","unstructured":"Seladji, Y., Bouissou, O.: Numerical abstract domain using support functions. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol.\u00a07871, pp. 155\u2013169. Springer, Heidelberg (2013)"},{"key":"18_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/978-3-642-24372-1_21","volume-title":"Automated Technology for Verification and Analysis","author":"P. Sotin","year":"2011","unstructured":"Sotin, P., Jeannet, B., V\u00e9drine, F., Goubault, E.: Policy iteration within logico-numerical abstract domains. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol.\u00a06996, pp. 290\u2013305. Springer, Heidelberg (2011)"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-02444-8_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,16]],"date-time":"2019-05-16T20:26:40Z","timestamp":1558038400000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-02444-8_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783319024431","9783319024448"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-02444-8_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}