{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:12:22Z","timestamp":1725549142669},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642119569"},{"type":"electronic","value":"9783642119576"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-11957-6_3","type":"book-chapter","created":{"date-parts":[[2010,3,7]],"date-time":"2010-03-07T19:55:38Z","timestamp":1267991738000},"page":"23-42","source":"Crossref","is-referenced-by-count":29,"title":["Coupling Policy Iteration with Semi-definite Relaxation to Compute Accurate Numerical Invariants in Static Analysis"],"prefix":"10.1007","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":"297","reference":[{"key":"3_CR1","unstructured":"Adje, A., Gaubert, S., Goubault, E.: Computing the smallest fixed point of nonexpansive mappings arising in game theory and static analysis of programs. Technical report, arXiv:0806.1160. In: Proceedings of MTNS 2008, Blacksburg, Virginia (July 2008)"},{"key":"3_CR2","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1137\/0805002","volume":"5","author":"F. Alizadeh","year":"1995","unstructured":"Alizadeh, F.: Interior point methods in semidefinite programming with applications to combinatorial optimization. SIAM Journal on Optimization\u00a05, 13\u201351 (1995)","journal-title":"SIAM Journal on Optimization"},{"key":"3_CR3","volume-title":"Asymptotic Cones and Functions in Optimization and Variational Inequalities","author":"A. Auslender","year":"2003","unstructured":"Auslender, A., Teboulle, M.: Asymptotic Cones and Functions in Optimization and Variational Inequalities. Springer, Heidelberg (2003)"},{"key":"3_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/11547662_4","volume-title":"Static Analysis","author":"R. Bagnara","year":"2005","unstructured":"Bagnara, R., Rodr\u00edguez-Carbonell, E., Zaffanella, E.: Generation of basic semi-algebraic invariants using convex polyhedra. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol.\u00a03672, pp. 19\u201334. Springer, Heidelberg (2005)"},{"key":"3_CR5","doi-asserted-by":"crossref","first-page":"238","DOI":"10.1145\/512950.512973","volume-title":"Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Los Angeles, California, pp. 238\u2013252. ACM Press, New York (1977)"},{"key":"3_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"3_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/b105073","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":"3_CR8","unstructured":"Feron, E., Alegre, F.: Control software analysis, part II: Closed-loop analysis. Technical report, arXiv:0812.1986 (2008)"},{"key":"3_CR9","unstructured":"Feret, J.: Numerical abstract domains for digital filters. In: International workshop on Numerical and Symbolic Abstract Domains, NSAD 2005 (2005)"},{"key":"3_CR10","unstructured":"Feron, E., Alegre, F.: Control software analysis, part I: Open-loop properties. Technical report, arXiv:0809.4812 (2008)"},{"key":"3_CR11","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":"3_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-540-79707-4_3","volume-title":"Formal Methods for Industrial Critical Systems","author":"E. Goubault","year":"2008","unstructured":"Goubault, E., Putot, S., Baufreton, P., Gassino, J.: Static analysis of the accuracy in control systems: Principles and experiments. In: Leue, S., Merino, P. (eds.) FMICS 2007. LNCS, vol.\u00a04916, pp. 3\u201320. Springer, Heidelberg (2008)"},{"key":"3_CR13","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":"3_CR14","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":"3_CR15","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1017\/S0962492902000144","volume":"12","author":"E. Hairer","year":"2003","unstructured":"Hairer, E., Lubich, C., Wanner, G.: Geometric numerical integration illustrated by the St\u00f6rmer\/Verlet method. Acta Numerica\u00a012, 399\u2013450 (2003)","journal-title":"Acta Numerica"},{"issue":"1","key":"3_CR16","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1137\/050622870","volume":"46","author":"C. Jansson","year":"2007","unstructured":"Jansson, C., Chaykin, D., Keil, C.: Rigorous error bounds for the optimal value in semidefinite programming. SIAM J. Numer. Anal.\u00a046(1), 180\u2013200 (2007)","journal-title":"SIAM J. Numer. Anal."},{"key":"3_CR17","unstructured":"Keil, C.: Lurupa - rigorous error bounds in linear programming. Algebraic and Numerical Algorithms and Computer-assisted Proofs (2005), \n                  \n                    http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2006\/445"},{"issue":"4","key":"3_CR18","doi-asserted-by":"publisher","first-page":"651","DOI":"10.1137\/070693709","volume":"49","author":"J.-B. Lasserre","year":"2007","unstructured":"Lasserre, J.-B.: A sum of squares approximations of nonnegative polynomials. SIAM Review\u00a049(4), 651\u2013669 (2007)","journal-title":"SIAM Review"},{"key":"3_CR19","unstructured":"Lfberg, J.: Yalmip: A toolbox for modeling and optimization in MATLAB. In: Proceedings of the CACSD Conference, Taipei, Taiwan (2004), \n                  \n                    http:\/\/control.ee.ethz.ch\/~joloef\/yalmip.php"},{"key":"3_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/978-3-540-24725-8_2","volume-title":"Programming Languages and Systems","author":"A. Min\u00e9","year":"2004","unstructured":"Min\u00e9, A.: Relational abstract domains for the detection of floating-point run-time errors. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol.\u00a02986, pp. 3\u201317. Springer, Heidelberg (2004)"},{"key":"3_CR21","unstructured":"Min\u00e9, A.: Weakly Relational Numerical Abstract Domains. PhD thesis, \u00c9cole Polytechnique, Palaiseau, France (December 2004), \n                  \n                    http:\/\/www.di.ens.fr\/~mine\/these\/these-color.pdf"},{"issue":"5","key":"3_CR22","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1016\/j.ipl.2004.05.004","volume":"91","author":"M. M\u00fcller-Olm","year":"2004","unstructured":"M\u00fcller-Olm, M., Seidl, H.: Computing polynomial program invariants. Inf. Process. Lett.\u00a091(5), 233\u2013244 (2004)","journal-title":"Inf. Process. Lett."},{"issue":"2, series B","key":"3_CR23","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/s10107-003-0387-5","volume":"96","author":"P. Parillo","year":"2003","unstructured":"Parillo, P.: Semidefinite programming relaxations for semialgebraic problems. Math. Prog.\u00a096(2, series B), 293\u2013320 (2003)","journal-title":"Math. Prog."},{"issue":"1","key":"3_CR24","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1016\/j.scico.2006.03.003","volume":"64","author":"E. Rodr\u00edguez-Carbonell","year":"2007","unstructured":"Rodr\u00edguez-Carbonell, E., Kapur, D.: Automatic generation of polynomial invariants of bounded degree using abstract interpretation. Sci. Comput. Program.\u00a064(1), 54\u201375 (2007)","journal-title":"Sci. Comput. Program."},{"key":"3_CR25","volume-title":"Convex Analysis","author":"R.T. Rockafellar","year":"1996","unstructured":"Rockafellar, R.T.: Convex Analysis. Princeton University Press, Princeton (1996)"},{"key":"3_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/11609773_8","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S. Sankaranarayanan","year":"2005","unstructured":"Sankaranarayanan, S., Colon, M., Sipma, H., Manna, Z.: Efficient strongly relational polyhedral analysis. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 111\u2013125. Springer, Heidelberg (2005)"},{"issue":"6","key":"3_CR27","first-page":"1","volume":"25","author":"N. Shor","year":"1987","unstructured":"Shor, N.: Quadratic optimization problems. Soviet J. of Computer and Systems Science\u00a025(6), 1\u201311 (1987)","journal-title":"Soviet J. of Computer and Systems Science"},{"key":"3_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1007\/978-3-540-30579-8_2","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S. Sankaranarayanan","year":"2005","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Scalable analysis of linear systems using mathematical programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 25\u201341. Springer, Heidelberg (2005)"},{"key":"3_CR29","doi-asserted-by":"publisher","first-page":"625","DOI":"10.1080\/10556789908805766","volume":"11-12","author":"J.F. Sturm","year":"1999","unstructured":"Sturm, J.F.: Using sedumi 1.02, a matlab toolbox for optimization over symmetric cones. Optimization Methods and Software\u00a011-12, 625\u2013653 (1999)","journal-title":"Optimization Methods and Software"},{"key":"3_CR30","doi-asserted-by":"crossref","DOI":"10.1137\/1.9780898718829","volume-title":"Lecture on Modern Convex Optimization: Analysis, Algorithm and Engineering Applications","author":"A. Ben Tal","year":"2001","unstructured":"Ben Tal, A., Nemirowski, A.: Lecture on Modern Convex Optimization: Analysis, Algorithm and Engineering Applications. SIAM, Philadelphia (2001)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-11957-6_3.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,23]],"date-time":"2020-11-23T21:45:47Z","timestamp":1606167947000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-11957-6_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642119569","9783642119576"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-11957-6_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}