{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,27]],"date-time":"2026-04-27T18:31:37Z","timestamp":1777314697929,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662482872","type":"print"},{"value":"9783662482889","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-48288-9_14","type":"book-chapter","created":{"date-parts":[[2015,9,1]],"date-time":"2015-09-01T02:26:24Z","timestamp":1441074384000},"page":"235-251","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["Property-based Polynomial Invariant Generation Using Sums-of-Squares Optimization"],"prefix":"10.1007","author":[{"given":"Assal\u00e9","family":"Adj\u00e9","sequence":"first","affiliation":[]},{"given":"Pierre-Lo\u00efc","family":"Garoche","sequence":"additional","affiliation":[]},{"given":"Victor","family":"Magron","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,9,2]]},"reference":[{"key":"14_CR1","unstructured":"Adj\u00e9, A.: Policy iteration in finite templates domain. In: 7th International Workshop on Numerical Software Verification (NSV 2012), July 2014"},{"key":"14_CR2","unstructured":"Adj\u00e9, A., Garoche, P.-L., Magron. V.: A Sums-of-squares extension of policy iterations. Technial report (2015)"},{"issue":"1","key":"14_CR3","first-page":"1","volume":"8","author":"A Adj\u00e9","year":"2011","unstructured":"Adj\u00e9, A., Gaubert, S., Goubault, E.: Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis. Log. Methods Comput. Sci. 8(1), 1\u201332 (2011)","journal-title":"Log. Methods Comput. Sci."},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"Ahmadi, A.A., Jungers, R.M.: Switched stability of nonlinear systems via sos-convex lyapunov functions and semidefinite programming. In: CDC 2013, pp. 727\u2013732 (2013)","DOI":"10.1109\/CDC.2013.6759968"},{"key":"14_CR5","series-title":"Applied Optimization","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/978-1-4757-3216-0_8","volume-title":"High Performance Optimization","author":"ED Andersen","year":"2000","unstructured":"Andersen, E.D., Andersen, K.D.: The mosek interior point optimizer for linear programming: an implementation of the homogeneous algorithm. In: Frenk, H., Roos, K., Terlaky, T., Zhang, S. (eds.) High Performance Optimization. Applied Optimization, vol. 33, pp. 197\u2013232. Springer, US (2000)"},{"key":"14_CR6","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. 3672, pp. 19\u201334. Springer, Heidelberg (2005)"},{"key":"14_CR7","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1016\/j.scico.2014.02.028","volume":"93","author":"D Cachera","year":"2014","unstructured":"Cachera, D., Jensen, T., Jobin, A., Kirchner, F.: Inference of polynomial invariants for imperative programs: a farewell to gr\u00f6bner bases. Sci. Comput. Program. 93, 89\u2013109 (2014)","journal-title":"Sci. Comput. Program."},{"key":"14_CR8","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. 3385, pp. 1\u201324. Springer, Heidelberg (2005)"},{"key":"14_CR9","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: Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 238\u2013252. ACM Press, Los Angeles, California, New York (1977)","DOI":"10.1145\/512950.512973"},{"issue":"2","key":"14_CR10","first-page":"128","volume":"17","author":"T Dang","year":"2012","unstructured":"Dang, T., Testylier, R.: Reachability analysis for polynomial dynamical systems using the bernstein expansion. Reliab. Comput. 17(2), 128\u2013152 (2012)","journal-title":"Reliab. Comput."},{"key":"14_CR11","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. 2986, pp. 33\u201348. Springer, Heidelberg (2004)"},{"issue":"3","key":"14_CR12","doi-asserted-by":"publisher","first-page":"796","DOI":"10.1137\/S1052623400366802","volume":"11","author":"JB Lasserre","year":"2001","unstructured":"Lasserre, J.B.: Global optimization with polynomials and the problem of moments. SIAM J. Optim. 11(3), 796\u2013817 (2001)","journal-title":"SIAM J. Optim."},{"key":"14_CR13","series-title":"The IMA Volumes in Mathematics and its Applications","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-0-387-09686-5_7","volume-title":"Emerging Applications of AlgebraicGeometry","author":"M Laurent","year":"2009","unstructured":"Laurent, M.: Sums of squares, moment matrices and optimization over polynomials. In: Putinar, M., Sullivant, S. (eds.) Emerging Applications of AlgebraicGeometry. The IMA Volumes in Mathematics and its Applications, vol. 149, pp. 157\u2013270. Springer, New York (2009)"},{"issue":"5","key":"14_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s11432-013-4961-z","volume":"57","author":"W Lin","year":"2014","unstructured":"Lin, W., Wu, M., Yang, Z., Zeng, Z.: Exact safety verification of hybrid systems using sums-of-squares representation. Sci. China Inf. Sci. 57(5), 1\u201313 (2014)","journal-title":"Sci. China Inf. Sci."},{"key":"14_CR15","first-page":"1","volume":"151","author":"V Magron","year":"2014","unstructured":"Magron, V., Allamigeon, X., Gaubert, S., Werner, B.: Certification of real inequalities - templates and sums of squares. Math. Program. Ser. B 151, 1\u201330 (2014). Volume on Polynomial Optimization","journal-title":"Math. Program. Ser. B"},{"issue":"5","key":"14_CR16","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. 91(5), 233\u2013244 (2004)","journal-title":"Inf. Process. Lett."},{"issue":"2","key":"14_CR17","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/s10107-003-0387-5","volume":"96","author":"PA Parrilo","year":"2003","unstructured":"Parrilo, P.A.: Semidefinite programming relaxations for semialgebraic problems. Math. Program. 96(2), 293\u2013320 (2003)","journal-title":"Math. Program."},{"key":"14_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/978-3-540-24743-2_32","volume-title":"Hybrid Systems: Computation and Control","author":"S Prajna","year":"2004","unstructured":"Prajna, S., Jadbabaie, A.: Safety verification of hybrid systems using barrier certificates. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 477\u2013492. Springer, Heidelberg (2004)"},{"issue":"1","key":"14_CR19","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. 64(1), 54\u201375 (2007)","journal-title":"Sci. Comput. Program."},{"key":"14_CR20","unstructured":"Roux, P., Garoche, P.-L.: A polynomial template abstract domain based on bernstein polynomials. In: Sixth International Workshop on Numerical Software Verification, NSV 2013 (2013)"},{"key":"14_CR21","doi-asserted-by":"crossref","unstructured":"Roux, P., Jobredeaux, R., Garoche, P.-L., Feron, E.: A generic ellipsoid abstract domain for linear time invariant systems. In: Dang, T., Mitchell, I.M. (eds.) HSCC, pp. 105\u2013114. ACM (2012)","DOI":"10.1145\/2185632.2185651"},{"key":"14_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/978-3-642-33386-6_12","volume-title":"Automated Technology for Verification and Analysis","author":"MA Ben Sassi","year":"2012","unstructured":"Ben Sassi, M.A., Testylier, R., Dang, T., Girard, A.: Reachability analysis of polynomial systems using linear programming relaxations. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 137\u2013151. Springer, Heidelberg (2012)"},{"issue":"6","key":"14_CR23","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1145\/1543135.1542501","volume":"44","author":"S Srivastava","year":"2009","unstructured":"Srivastava, S., Gulwani, S.: Program verification using templates over predicate abstraction. SIGPLAN Not. 44(6), 223\u2013234 (2009)","journal-title":"SIGPLAN Not."},{"issue":"1","key":"14_CR24","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1137\/1038003","volume":"38","author":"L Vandenberghe","year":"1994","unstructured":"Vandenberghe, L., Boyd, S.: Semidefinite programming. SIAM Rev. 38(1), 49\u201395 (1994)","journal-title":"SIAM Rev."},{"issue":"1","key":"14_CR25","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1137\/050623802","volume":"17","author":"H Waki","year":"2006","unstructured":"Waki, H., Kim, S., Kojima, M., Muramatsu, M.: Sums of squares and semidefinite programming relaxations for polynomial optimization problems with structured sparsity. SIAM J. Optim. 17(1), 218\u2013242 (2006)","journal-title":"SIAM J. Optim."},{"key":"14_CR26","unstructured":"Yamashita, M., Fujisawa, K., Nakata, K., Nakata, M., Fukuda, M., Kobayashi, K., Goto, K.: A high-performance software package for semidefinite programs : Sdpa7. Depatrment of Information Sciences, Tokyo Institute of Technology, Tokyo, Japan, Technical report (2010)"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-48288-9_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,1]],"date-time":"2023-02-01T18:08:56Z","timestamp":1675274936000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-48288-9_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662482872","9783662482889"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-48288-9_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"2 September 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}