{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T01:04:39Z","timestamp":1784768679157,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540242970","type":"print"},{"value":"9783540305798","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-30579-8_1","type":"book-chapter","created":{"date-parts":[[2010,12,20]],"date-time":"2010-12-20T16:45:34Z","timestamp":1292863534000},"page":"1-24","source":"Crossref","is-referenced-by-count":111,"title":["Proving Program Invariance and Termination by Parametric Abstraction, Lagrangian Relaxation and Semidefinite Programming"],"prefix":"10.1007","author":[{"given":"Patrick","family":"Cousot","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"1_CR1","unstructured":"Benson, S., Ye, Y.: DSDP4: A software package implementing the dual-scaling algorithm for semidefinite programming. Technical Report ANL\/MCS-TM-255, Argonne National Laboratory (2002)"},{"key":"1_CR2","doi-asserted-by":"crossref","DOI":"10.1137\/1.9781611970777","volume-title":"Linear Matrix Inequalities in System and Control Theory","author":"S. Boyd","year":"1994","unstructured":"Boyd, S., Ghaoui, L.E., F\u00e9ron, \u00c9., Balakrishnan, V.: Linear Matrix Inequalities in System and Control Theory. SIAM, Philadelphia (1994)"},{"issue":"1","key":"1_CR3","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/S0167-6423(99)00008-8","volume":"35","author":"J. Brauburger","year":"1999","unstructured":"Brauburger, J., Giesl, J.: Approximating the domains of functional and imperative programs. Sci. Comput. Programming\u00a035(1), 113\u2013136 (1999)","journal-title":"Sci. Comput. Programming"},{"issue":"2","key":"1_CR4","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/s10107-002-0352-8","volume":"95","author":"S. Burer","year":"2003","unstructured":"Burer, S., Monteiro, R.: A nonlinear programming algorithm for solving semidefinite programs via low-rank factorization. Mathematical Programming (series B)\u00a095(2), 329\u2013357 (2003)","journal-title":"Mathematical Programming (series B)"},{"key":"1_CR5","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1016\/S0747-7171(08)80152-6","volume":"12","author":"G. Collins","year":"1991","unstructured":"Collins, G., Hong, H.: Partial cylindrical algebraic decomposition for quantifier elimination. J. Symb. Comput.\u00a012, 299\u2013328 (1991)","journal-title":"J. Symb. Comput."},{"key":"1_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/3-540-45319-9_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Col\u00f3n","year":"2001","unstructured":"Col\u00f3n, M., Sipma, H.: Synthesis of linear ranking functions. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 67\u201381. Springer, Heidelberg (2001)"},{"key":"1_CR7","unstructured":"Cousot, P.: M\u00e9thodes it\u00e9ratives de construction et d\u2019approximation de points fixes d\u2019op\u00e9rateurs monotones sur un treillis, analyse s\u00e9mantique de programmes. Th\u00e8se d\u2019Etat \u00e8s sciences math\u00e9matiques, Univ. scient. et m\u00e9d. de Grenoble (1978)"},{"key":"1_CR8","first-page":"238","volume-title":"4th POPL","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: 4th POPL, pp. 238\u2013252. ACM Press, New York (1977)"},{"key":"1_CR9","first-page":"237","volume-title":"IFIP Conf. on Formal Description of Programming Concepts, St- Andrews","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Static determination of dynamic properties of recursive procedures. In: IFIP Conf. on Formal Description of Programming Concepts, St- Andrews, pp. 237\u2013277. North-Holland, Amsterdam (1977)"},{"key":"1_CR10","first-page":"269","volume-title":"6th POPL","author":"P. Cousot","year":"1979","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: 6th POPL, pp. 269\u2013282. ACM Press, New York (1979)"},{"key":"1_CR11","first-page":"277","volume-title":"Algebraic Methods in Semantics, ch. 8","author":"P. Cousot","year":"1985","unstructured":"Cousot, P., Cousot, R.: \u2018\u00c0 la Floyd\u2019 induction principles for proving inevitability properties of programs. In: Algebraic Methods in Semantics, ch. 8, pp. 277\u2013312. Cambridge U. Press, Cambridge (1985)"},{"issue":"2-3","key":"1_CR12","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/0743-1066(92)90030-7","volume":"13","author":"P. Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation and application to logic programs12. J. Logic Programming\u00a013(2-3), 103\u2013179 (1992)","journal-title":"J. Logic Programming"},{"issue":"4","key":"1_CR13","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1093\/logcom\/2.4.511","volume":"2","author":"P. Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation frameworks. J. Logic and Comp.\u00a02(4), 511\u2013547 (1992)","journal-title":"J. Logic and Comp."},{"key":"1_CR14","first-page":"84","volume-title":"5th POPL","author":"P. Cousot","year":"1978","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: 5th POPL, pp. 84\u201397. ACM Press, New York (1978)"},{"key":"1_CR15","unstructured":"F\u00e9ron, \u00c9.: Abstraction mechanisms across the board: A short introduction. Workshop on Robustness, Abstractions and Computations, Philadelphia, March 18 (2004)"},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"Floyd, R.: Assigning meaning to programs. In: Proc. Symposium in Applied Mathematics. AMS, vol.\u00a019, pp. 19\u201332 (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"1_CR17","unstructured":"Gahinet, P., Nemirovski, A., Laub, A., Chilali, M.: LMI Control Toolbox for use with Matlab\n                           \u00ae, user\u2019s guide (1995)"},{"key":"1_CR18","first-page":"74","volume-title":"30th POPL","author":"S. Gulwani","year":"2003","unstructured":"Gulwani, S., Necula, G.: Discovering affine equalities using random interpretation. In: 30th POPL, pp. 74\u201384. ACM Press, New York (2003)"},{"issue":"10","key":"1_CR19","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C. Hoare","year":"1969","unstructured":"Hoare, C.: An axiomatic basis for computer programming. Comm. ACM\u00a012(10), 576\u2013580 (1969)","journal-title":"Comm. ACM"},{"key":"1_CR20","unstructured":"Jeannet, B.: New Polka, \n                    \n                      http:\/\/www.irisa.fr\/prive\/bjeannet\/newpolka.html"},{"key":"1_CR21","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/BF00268497","volume":"6","author":"M. Karr","year":"1976","unstructured":"Karr, M.: Affine relationships among variables of a program. Acta Informat.\u00a06, 133\u2013151 (1976)","journal-title":"Acta Informat."},{"key":"1_CR22","unstructured":"Ko\u010dvara, M., Stingl, M.: Penbmi User\u2019s Guide, Version 1.1 (2004)"},{"key":"1_CR23","unstructured":"L\u00f6fberg, J.: YALMIP, \n                    \n                      http:\/\/control.ee.ethz.ch\/~joloef\/yalmip.msql"},{"key":"1_CR24","volume-title":"Mathematical theory of computation","author":"Z. Manna","year":"1974","unstructured":"Manna, Z.: Mathematical theory of computation. McGraw Hill, New York (1974)"},{"key":"1_CR25","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/BF01966091","volume":"6","author":"P. Naur","year":"1966","unstructured":"Naur, P.: Proofs of algorithms by general snapshots. BIT\u00a06, 310\u2013316 (1966)","journal-title":"BIT"},{"key":"1_CR26","doi-asserted-by":"crossref","first-page":"405","DOI":"10.1007\/978-1-4757-3216-0_17","volume-title":"High Performance Optimization","author":"Y. Nesterov","year":"2000","unstructured":"Nesterov, Y.: Squared functional systems and optimization problems. In: High Performance Optimization, pp. 405\u2013440. Kluwer Acad. Pub., Dordrecht (2000)"},{"issue":"6","key":"1_CR27","first-page":"1084","volume":"24","author":"Y. Nesterov","year":"1988","unstructured":"Nesterov, Y., Nemirovskii, A.: Polynomial barrier methods in convex programming. \u00c8konom. i Mat. Metody\u00a024(6), 1084\u20131091 (1988)","journal-title":"\u00c8konom. i Mat. Metody"},{"issue":"2","key":"1_CR28","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/s10107-003-0387-5","volume":"96","author":"P. Parrilo","year":"2003","unstructured":"Parrilo, P.: Semidefinite programming relaxations for semialgebraic problems. Mathematical Programming\u00a096(2), 293\u2013320 (2003)","journal-title":"Mathematical Programming"},{"key":"1_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-540-24622-0_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Podelski","year":"2004","unstructured":"Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 239\u2013251. Springer, Heidelberg (2004)"},{"key":"1_CR30","unstructured":"Prajna, S., Papachristodoulou, A., Seiler, P., Parrilo, P.: SOStools: Sum of squares optimization toolbox for Matlab (2004)"},{"key":"1_CR31","doi-asserted-by":"crossref","unstructured":"Sturm, J.: Using SeDuMi 1.02, a Matlab toolbox for optimization over symmetric cones. Optimization Methods and Software\u00a011\u201312, 625\u2013653 (1999)","DOI":"10.1080\/10556789908805766"},{"key":"1_CR32","doi-asserted-by":"publisher","first-page":"545","DOI":"10.1080\/10556789908805762","volume":"11","author":"K. Toh","year":"1999","unstructured":"Toh, K., Todd, M., T\u00fct\u00fcnc\u00fc, R.: SDPT3\u2013a Matlab software package for semidefinite programming. Optimization Methods and Software\u00a011, 545\u2013581 (1999)","journal-title":"Optimization Methods and Software"},{"key":"1_CR33","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1016\/0167-6911(92)90034-P","volume":"19","author":"V. Yakubovich","year":"1992","unstructured":"Yakubovich, V.: Nonconvex optimization problem: The infinite-horizon linearquadratic control problem with quadratic constraints. Systems Cosntrol Lett.\u00a019, 13\u201322 (1992)","journal-title":"Systems Cosntrol Lett."}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30579-8_1.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T03:31:21Z","timestamp":1620012681000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30579-8_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540242970","9783540305798"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30579-8_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}