{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,24]],"date-time":"2025-06-24T15:47:41Z","timestamp":1750780061491},"publisher-location":"Berlin, Heidelberg","reference-count":63,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662534120"},{"type":"electronic","value":"9783662534137"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-662-53413-7_21","type":"book-chapter","created":{"date-parts":[[2016,8,30]],"date-time":"2016-08-30T07:57:11Z","timestamp":1472543831000},"page":"424-446","source":"Crossref","is-referenced-by-count":12,"title":["Validating Numerical Semidefinite Programming Solvers for Polynomial Invariants"],"prefix":"10.1007","author":[{"given":"Pierre","family":"Roux","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yuen-Lam","family":"Voronin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sriram","family":"Sankaranarayanan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,8,31]]},"reference":[{"key":"21_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1007\/978-3-662-48288-9_14","volume-title":"Static Analysis","author":"A Adj\u00e9","year":"2015","unstructured":"Adj\u00e9, A., Garoche, P.-L., Magron, V.: Property-based polynomial invariant generation using sums-of-squares optimization. In: Blazy, S., Jensen, T. (eds.) SAS 2015. LNCS, vol. 9291, pp. 235\u2013251. Springer, Heidelberg (2015)"},{"key":"21_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. 6012, pp. 23\u201342. Springer, Heidelberg (2010)"},{"key":"21_CR3","doi-asserted-by":"crossref","unstructured":"Ahmadi, A.A., Majumdar, A.: DSOS and SDSOS optimization: LP and SOCP-based alternatives to sum of squares optimization. In: Annual Conference on Information Sciences and Systems (CISS) (2014)","DOI":"10.1109\/CISS.2014.6814141"},{"key":"21_CR4","doi-asserted-by":"crossref","unstructured":"Allamigeon, X., Gaubert, S., Goubault, E., Putot, S., Stott, N.: A scalable algebraic method to infer quadratic invariants of switched systems. In: EMSOFT (2015)","DOI":"10.1109\/EMSOFT.2015.7318262"},{"key":"21_CR5","series-title":"International Series in Operations Research & Management Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-1-4614-0769-0_1","volume-title":"Handbook on semidefinite, conic and polynomial optimization","author":"MF Anjos","year":"2012","unstructured":"Anjos, M.F., Lasserre, J.B.: Introduction to semidefinite, conic and polynomial optimization. In: Anjos, M.F., Lasserre, J.B. (eds.) Handbook on semidefinite, conic and polynomial optimization. International Series in Operations Research & Management Science, vol. 166, pp. 1\u201322. Springer, New York (2012)"},{"key":"21_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. 3672, pp. 19\u201334. Springer, Heidelberg (2005)"},{"key":"21_CR7","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-33099-2","volume-title":"Algorithms in Real Algebraic Geometry","author":"S Basu","year":"2006","unstructured":"Basu, S., Pollock, R., Roy, M.-F.: Algorithms in Real Algebraic Geometry, vol. 10. Springer, Heidelberg (2006)"},{"key":"21_CR8","doi-asserted-by":"crossref","unstructured":"Ben Sassi, M.A., Sankaranarayanan, S., Chen, X., Abraham, E.: Linear relaxations of polynomial positivity for polynomial Lyapunov function synthesis. IMA J. Math. Control Inf. (2015)","DOI":"10.1093\/imamci\/dnv003"},{"key":"21_CR9","unstructured":"Bernstein, S.N.: D\u00e9monstration du th\u00e9or\u00e9me de Weierstrass fond\u00e9e sur le calcul des probabilit\u00e9s. Communcations de la Soci\u00e9t\u00e9 Math\u00e9matique de Kharkov 2 (1912)"},{"key":"21_CR10","doi-asserted-by":"crossref","unstructured":"Borchers, B.: CSDP, a C library for semidefinite programming. Optim. Methods Softw. (1999)","DOI":"10.1080\/10556789908805765"},{"key":"21_CR11","doi-asserted-by":"crossref","unstructured":"Borwein, J.M., Wolkowicz, H.: Facial reduction for a cone-convex programming problem. J. Austral. Math. Soc. Ser. A (1980\/1981)","DOI":"10.1017\/S1446788700017250"},{"key":"21_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-662-49674-9_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Chakarov","year":"2016","unstructured":"Chakarov, A., Voronin, Y.-L., Sankaranarayanan, S.: Deductive proofs of almost sure persistence and recurrence properties. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 260\u2013279. Springer, Heidelberg (2016). doi: 10.1007\/978-3-662-49674-9_15"},{"key":"21_CR13","doi-asserted-by":"crossref","unstructured":"Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Automata Theory and Formal Languages (1975)","DOI":"10.1007\/3-540-07407-4_17"},{"key":"21_CR14","doi-asserted-by":"crossref","unstructured":"Collins, G.E., Hong, H.: Partial cylindrical algebraic decomposition for quantifier elimination. J. Symbolic Comput. (1991)","DOI":"10.1016\/S0747-7171(08)80152-6"},{"key":"21_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. 3385, pp. 1\u201324. Springer, Heidelberg (2005)"},{"key":"21_CR16","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"},{"key":"21_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"34","DOI":"10.1007\/978-3-642-25318-8_6","volume-title":"Programming Languages and Systems","author":"T Dang","year":"2011","unstructured":"Dang, T., Gawlitza, T.M.: Template-based unbounded time verification of affine hybrid automata. In: Yang, H. (ed.) APLAS 2011. LNCS, vol. 7078, pp. 34\u201349. Springer, Heidelberg (2011)"},{"key":"21_CR18","unstructured":"Demmel, J.: On floating point errors in Cholesky. Department of Computer Science, University of Tennessee, Knoxville, TN, USA, Lapack working note (1989)"},{"key":"21_CR19","doi-asserted-by":"crossref","unstructured":"Dolzmann, A., Sturm, T.: REDLOG: computer algebra meets computer logic. ACM SIGSAM Bull. (1997)","DOI":"10.1145\/261320.261324"},{"key":"21_CR20","unstructured":"D\u00fcr, M., Jargalsaikhan, B., Still, G.: The Slater condition is generic in linear conic programming (2012)"},{"key":"21_CR21","doi-asserted-by":"crossref","unstructured":"Farouki, R.T.: The Bernstein polynomial basis: a centennial retrospective. Comput. Aided Geom. Des. (2012)","DOI":"10.1016\/j.cagd.2012.03.001"},{"key":"21_CR22","unstructured":"F\u00e9ron, \u00c9.: From control systems to control software. IEEE Control Syst. (2010)"},{"key":"21_CR23","doi-asserted-by":"crossref","unstructured":"Fr\u00e4nzle, M., Herde, C., Teige, T., Ratschan, S., Schubert, T.: Efficient solving of large non-linear arithmetic constraint systems with complex Boolean structure. J. Satisfiability, Boolean Model. Comput., Special Issue on SAT\/CP Integration (2007)","DOI":"10.3233\/SAT190012"},{"key":"21_CR24","doi-asserted-by":"crossref","unstructured":"Gao, S., Kong, S., Clarke, E.M.: dReal: An SMT solver for nonlinear theories over the reals. In: International Conference on Automated Deduction (CADE) (2013)","DOI":"10.1007\/978-3-642-38574-2_14"},{"key":"21_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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, \u00c9., Taly, A., Zennou, S.: Static analysis by policy iteration on relational domains. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 237\u2013252. Springer, Heidelberg (2007)"},{"key":"21_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. 4421, pp. 300\u2013315. Springer, Heidelberg (2007)"},{"key":"21_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1007\/978-3-642-19718-5_13","volume-title":"Programming Languages and Systems","author":"TM Gawlitza","year":"2011","unstructured":"Gawlitza, T.M., Monniaux, D.: Improving strategies via SMT solving. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 236\u2013255. Springer, Heidelberg (2011)"},{"key":"21_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1007\/978-3-642-15769-1_17","volume-title":"Static Analysis","author":"TM 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. 6337, pp. 271\u2013286. Springer, Heidelberg (2010)"},{"key":"21_CR29","doi-asserted-by":"crossref","unstructured":"Handelman, D.: Representing polynomials by positive linear functions on compact convex polyhedra. Pacific J. Math. (1988)","DOI":"10.2140\/pjm.1988.132.35"},{"key":"21_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1007\/978-3-540-74591-4_9","volume-title":"Theorem Proving in Higher Order Logics","author":"J Harrison","year":"2007","unstructured":"Harrison, J.: Verifying nonlinear real formulas via sums of squares. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 102\u2013118. Springer, Heidelberg (2007)"},{"key":"21_CR31","unstructured":"H\u00e4rter, V., Jansson, C., Lange, M.: VSDP: verified semidefinite programming. http:\/\/www.ti3.tuhh.de\/jansson\/vsdp\/ . Accessed 28 Mar 2016"},{"key":"21_CR32","unstructured":"Henrion, D., Naldi, S., Din, M., Safey El Din, M.: Exact algorithms for linear matrix inequalities. arXiv preprint (2015). arXiv:1508.03715"},{"key":"21_CR33","unstructured":"IEEE Computer Society. IEEE Standard for Floating-Point Arithmetic. IEEE Standard 754\u20132008 (2008)"},{"key":"21_CR34","doi-asserted-by":"crossref","unstructured":"Jansson, C., Chaykin, D., Keil, C.: Rigorous error bounds for the optimal value in semidefinite programming. SIAM J. Numer. Anal. (2007)","DOI":"10.1137\/050622870"},{"key":"21_CR35","doi-asserted-by":"crossref","unstructured":"Kaltofen, E., Li, B., Yang, Z., Zhi, L.: Exact certification in global polynomial optimization via sums-of-squares of rational functions with rational coefficients. J. Symb. Comput. (2012)","DOI":"10.1016\/j.jsc.2011.08.002"},{"key":"21_CR36","doi-asserted-by":"crossref","unstructured":"Lasserre, J.B.: Global optimization with polynomials and the problem of moments. SIAM J. Optim. (2001)","DOI":"10.1137\/S1052623400366802"},{"key":"21_CR37","doi-asserted-by":"crossref","unstructured":"L\u00f6fberg, J.: Pre- and post-processing sum-of-squares programs in practice. IEEE Trans. Autom. Control (2009)","DOI":"10.1109\/TAC.2009.2017144"},{"key":"21_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/978-3-662-49122-5_8","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Mar\u00e9chal","year":"2016","unstructured":"Mar\u00e9chal, A., Fouilh\u00e9, A., King, T., Monniaux, D., P\u00e9rin, M.: Polyhedral approximation of multivariate polynomials using Handelman\u2019s theorem. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 166\u2013184. Springer, Heidelberg (2016). doi: 10.1007\/978-3-662-49122-5_8"},{"key":"21_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1007\/978-3-642-22863-6_19","volume-title":"Interactive Theorem Proving","author":"D Monniaux","year":"2011","unstructured":"Monniaux, D., Corbineau, P.: On the generation of positivstellensatz witnesses in degenerate cases. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 249\u2013264. Springer, Heidelberg (2011)"},{"key":"21_CR40","unstructured":"MOSEK ApS. The MOSEK C optimizer API manual Version 7.1 (Revision 40) (2015)"},{"key":"21_CR41","doi-asserted-by":"crossref","unstructured":"Nakata, M.: A numerical evaluation of highly accurate multiple-precision arithmetic version of semidefinite programming solver: SDPA-GMP, -QD and -DD. In: Computer-Aided Control System Design (2010)","DOI":"10.1109\/CACSD.2010.5612693"},{"key":"21_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"415","DOI":"10.1007\/978-3-319-21690-4_24","volume-title":"Computer Aided Verification","author":"M Oulamara","year":"2015","unstructured":"Oulamara, M., Venet, A.J.: Abstract interpretation with higher-dimensional ellipsoids and conic extrapolation. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 415\u2013430. Springer, Heidelberg (2015)"},{"key":"21_CR43","doi-asserted-by":"crossref","unstructured":"Parrilo, P.A.: Semidefinite programming relaxations for semialgebraic problems. Math. Program. (2003)","DOI":"10.1007\/s10107-003-0387-5"},{"key":"21_CR44","unstructured":"Permenter, F., Parrilo, P.: Partial facial reduction: simplified, equivalent SDPs via approximations of the PSD cone. arXiv preprint (2014). arXiv:1408.4685"},{"key":"21_CR45","doi-asserted-by":"crossref","unstructured":"Peyrl, H., Parrilo, P.A.: Computing sum of squares decompositions with rational coefficients. Theor. Comput. Sci. (2008)","DOI":"10.1016\/j.tcs.2008.09.025"},{"key":"21_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"485","DOI":"10.1007\/978-3-642-02959-2_35","volume-title":"Automated Deduction \u2013 CADE-22","author":"A Platzer","year":"2009","unstructured":"Platzer, A., Quesel, J.-D., R\u00fcmmer, P.: Real world verification. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol. 5663, pp. 485\u2013501. Springer, Heidelberg (2009)"},{"key":"21_CR47","doi-asserted-by":"crossref","unstructured":"Prajna, S., Jadbabaie, A.: Safety verification using barrier certificates. In: HSCC (2004)","DOI":"10.1109\/CDC.2004.1428804"},{"key":"21_CR48","doi-asserted-by":"crossref","unstructured":"Putinar, M.: Positive polynomials on compact semi-algebraic sets. Indiana Univ. Math. J. (1993)","DOI":"10.1512\/iumj.1993.42.42045"},{"key":"21_CR49","doi-asserted-by":"crossref","unstructured":"Roux, P.: Formal proofs of rounding error bounds. J. Autom. Reasoning (2015)","DOI":"10.1007\/s10817-015-9339-z"},{"key":"21_CR50","doi-asserted-by":"crossref","unstructured":"Rump, S.M.: Verification of positive definiteness. BIT Numer. Math. (2006)","DOI":"10.1007\/s10543-006-0056-1"},{"key":"21_CR51","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Sipma, H., Manna, Z.: Constructing invariants for hybrid systems. Formal Meth. Syst. Des. (2008)","DOI":"10.1007\/s10703-007-0046-1"},{"key":"21_CR52","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. 3385, pp. 25\u201341. Springer, Heidelberg (2005)"},{"key":"21_CR53","unstructured":"Schmieta, S.H., Pataki, G.: Reporting solution quality for the DIMACS library of mixed semidefinite-quadratic-linear programs. http:\/\/dimacs.rutgers.edu\/Challenges\/Seventh\/Instances\/error_report.html . Accessed 23 Mar 2016"},{"key":"21_CR54","doi-asserted-by":"crossref","unstructured":"Sherali, H.D., Tuncbilek, Cihan H. C.H. : A global optimization algorithm for polynomial programming using a reformulation-linearization technique. J. Glob. Optim. (1991)","DOI":"10.1007\/BF00121304"},{"key":"21_CR55","unstructured":"Shor, N.Z.: Class of global minimum bounds on polynomial functions. Cybernetics (1987). Originally in Russian: Kibernetika (1987)"},{"key":"21_CR56","doi-asserted-by":"crossref","unstructured":"Sturm, J.F.: Using SeDuMi 1.02, a MATLAB toolbox for optimization over symmetric cones. Optim. Methods Softw. (1999)","DOI":"10.1080\/10556789908805766"},{"key":"21_CR57","doi-asserted-by":"crossref","unstructured":"Tarski, A.: A decision method for elementary algebra and geometry. Univ. of California Press, Berkeley, Technical report (1951)","DOI":"10.1525\/9780520348097"},{"key":"21_CR58","doi-asserted-by":"crossref","unstructured":"Tuncel, L.: Polyhedral and semidefinite programming methods in combinatorial optimization. Am. Math. Soc. (2010)","DOI":"10.1090\/fim\/027"},{"key":"21_CR59","doi-asserted-by":"crossref","unstructured":"T\u00fct\u00fcnc\u00fc, R.H., Toh, K.C., Todd, M.J.: Solving semidefinite-quadratic-linear programs using SDPT3. Math. Program. (2003)","DOI":"10.1007\/s10107-002-0347-5"},{"key":"21_CR60","doi-asserted-by":"crossref","unstructured":"Waki, H., Nakata, M., Muramatsu, M.: Strange behaviors of interior-point methods for solving semidefinite programming problems in polynomial optimization. Comput. Optim. Appl. (2011)","DOI":"10.1007\/s10589-011-9437-8"},{"key":"21_CR61","doi-asserted-by":"crossref","unstructured":"Weispfenning, V.: Quantifier elimination for real algebra\u2013the quadratic case and beyond. In: Applied Algebra and Error-Correcting Codes (AAECC) (1997)","DOI":"10.1007\/s002000050055"},{"key":"21_CR62","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-4381-7","volume-title":"Handbook of Semidefinite Programming","author":"H Wolkowicz","year":"2000","unstructured":"Wolkowicz, H., Saigal, R., Vandenberghe, L.: Handbook of Semidefinite Programming. Kluwer Academic Publishers, Boston (2000)"},{"key":"21_CR63","unstructured":"Yamashita, M., Fujisawa, K., Nakata, K., Nakata, M., Fukuda, M., Kobayashi, K., Goto, K.: A high-performance software package for semidefinite programs: SDPA\u00a07. Technical report B-460, Tokyo Institute of Technology (2010)"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-53413-7_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,7]],"date-time":"2022-07-07T06:44:33Z","timestamp":1657176273000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-53413-7_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662534120","9783662534137"],"references-count":63,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-53413-7_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}