{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,10]],"date-time":"2024-07-10T10:52:24Z","timestamp":1720608744719},"reference-count":29,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Computer Languages, Systems & Structures"],"published-print":{"date-parts":[[2017,1]]},"DOI":"10.1016\/j.cl.2015.12.002","type":"journal-article","created":{"date-parts":[[2015,12,18]],"date-time":"2015-12-18T00:14:12Z","timestamp":1450397652000},"page":"44-61","update-policy":"http:\/\/dx.doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":0,"special_numbering":"P1","title":["Automatic synthesis of k-inductive piecewise quadratic invariants for switched affine control programs"],"prefix":"10.1016","volume":"47","author":[{"given":"Assal\u00e9","family":"Adj\u00e9","sequence":"first","affiliation":[]},{"given":"Pierre-Lo\u00efc","family":"Garoche","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.cl.2015.12.002_bib1","doi-asserted-by":"crossref","unstructured":"Adj\u00e9 A, Garoche P-L. Automatic synthesis of piecewise linear quadratic invariants for programs. In: D\u05f3Souza D, Lal A, Guldstrand Larsen K, editors. Verification, model checking, and abstract interpretation\u201416th international conference, VMCAI 2015, Mumbai, India, January 12\u201314, 2015. Proceedings, Lecture notes in computer science, vol. 8931. Springer; 2015. p. 99\u2013116.","DOI":"10.1007\/978-3-662-46081-8_6"},{"key":"10.1016\/j.cl.2015.12.002_bib2","unstructured":"Allamigeon X. Static analysis of memory manipulations by abstract interpretation\u2014algorithmics of tropical polyhedra, and application to abstract interpretation [Ph.D. thesis]. \u00c9cole Polytechnique, Palaiseau, France; November 2009."},{"issue":"255","key":"10.1016\/j.cl.2015.12.002_bib3","doi-asserted-by":"crossref","first-page":"687","DOI":"10.1016\/S0304-3975(00)00399-6","article-title":"Deciding stability and mortality of piecewise affine dynamical systems","volume":"1\u20132","author":"Blondel","year":"2001","journal-title":"Theoret Comput Sci A"},{"key":"10.1016\/j.cl.2015.12.002_bib4","doi-asserted-by":"crossref","unstructured":"Bertrane J, Cousot P, Cousot R, Feret J, Mauborgne L, Min A, et al. Static analysis by abstract interpretation of embedded critical software. In: ACM SIGSOFT Software Engineering Notes, vol. 36, no. 1; 2011. p. 1\u20138.","DOI":"10.1145\/1921532.1921553"},{"key":"10.1016\/j.cl.2015.12.002_bib5","doi-asserted-by":"crossref","unstructured":"Biswas P, Grieder P, L\u00f6fberg J, Morari M. A survey on stability analysis of discrete-time piecewise affine systems. In: IFAC world congress. Prague, Czech Republic; July 2005.","DOI":"10.3182\/20050703-6-CZ-1902.00332"},{"key":"10.1016\/j.cl.2015.12.002_bib6","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. New York, NY, Los Angeles, CA: ACM Press; 1977. p. 238\u201352.","DOI":"10.1145\/512950.512973"},{"key":"10.1016\/j.cl.2015.12.002_bib7","series-title":"POPL","first-page":"84","article-title":"Automatic discovery of linear restraints among variables of a program","author":"Cousot","year":"1978"},{"key":"10.1016\/j.cl.2015.12.002_bib8","first-page":"176","article-title":"Generalizing the template polyhedral domain","volume":"vol. 6602","author":"Col\u00f3n","year":"2011"},{"key":"10.1016\/j.cl.2015.12.002_bib9","doi-asserted-by":"crossref","unstructured":"Colon M, Sankaranarayanan S, Sipma H. Linear invariant generation using non-linear constraint solving. In: Computer-aided verification (CAV), Lecture notes in computer science, vol. 2725. Springer-Verlag; 2003. p. 420\u201333.","DOI":"10.1007\/978-3-540-45069-6_39"},{"key":"10.1016\/j.cl.2015.12.002_bib10","first-page":"33","article-title":"Static analysis of digital filters","volume":"vol. 2986","author":"Feret","year":"2004"},{"key":"10.1016\/j.cl.2015.12.002_bib11","unstructured":"Fil\u00e9 G, Ranzato F. Improving abstract interpretations by systematic lifting to the powerset. In: Logic programming. Proceedings of the 1994 international symposium, Ithaca, NY, USA; November 13\u201317, 1994. p. 655\u201369."},{"key":"10.1016\/j.cl.2015.12.002_bib12","first-page":"627","article-title":"The zonotope abstract domain taylor1+","volume":"vol. 5643","author":"Ghorbal","year":"2009"},{"issue":"12","key":"10.1016\/j.cl.2015.12.002_bib13","doi-asserted-by":"crossref","first-page":"1416","DOI":"10.1016\/j.jsc.2011.12.048","article-title":"Abstract interpretation meets convex optimization","volume":"47","author":"Gawlitza","year":"2012","journal-title":"J Symb Comput"},{"issue":"1","key":"10.1016\/j.cl.2015.12.002_bib14","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF02355379","article-title":"Conditionally definite matrices","volume":"98","author":"Ikramov","year":"2000","journal-title":"J Math Sci"},{"key":"10.1016\/j.cl.2015.12.002_bib15","doi-asserted-by":"crossref","unstructured":"Johansson M. On modeling, analysis and design of piecewise linear control systems. In: Proceedings of the 2003 international symposium on circuits and systems, 2003. ISCAS \u05f303, vol. 3; May 2003. p. III\u2013646\u2013III\u2013649.","DOI":"10.1109\/ISCAS.2003.1205102"},{"key":"10.1016\/j.cl.2015.12.002_bib16","unstructured":"Kahsai T, Tinelli c. Pkind: a parallel k-induction based model checker. In: Barnat J, Heljanko K, editors. Proceedings 10th international workshop on parallel and distributed methods in verification, PDMC 2011, Snowbird, UT, USA, vol. 72 of EPTCS; July 14, 2011, p. 55\u201362."},{"issue":"5","key":"10.1016\/j.cl.2015.12.002_bib17","doi-asserted-by":"crossref","first-page":"868","DOI":"10.1109\/TAC.2007.895924","article-title":"Uniformly stabilizing sets of switching sequences for switched linear systems","volume":"52","author":"Lee","year":"2007","journal-title":"IEEE Trans Automat Contr"},{"key":"10.1016\/j.cl.2015.12.002_bib18","doi-asserted-by":"crossref","unstructured":"Lee J-W, Dullerud GE. Joint synthesis of switching and feedback for linear systems in discrete time. In: Caccamo M, Frazzoli E, Grosu R, editors. Proceedings of the 14th ACM international conference on hybrid systems: computation and control, HSCC 2011, Chicago, IL, USA, April 12-14. ACM; 2011. p. 201\u201310.","DOI":"10.1145\/1967701.1967731"},{"key":"10.1016\/j.cl.2015.12.002_bib19","doi-asserted-by":"crossref","unstructured":"Lee J-W, Dullerud GE, Khargonekar PP. An output regulation problem for switched linear systems in discrete time. In: Proceedings of the 46th IEEE conference on decision and control; 2007. p. 4993\u20138.","DOI":"10.1109\/CDC.2007.4434817"},{"key":"10.1016\/j.cl.2015.12.002_bib20","doi-asserted-by":"crossref","unstructured":"Mignone D, Ferrari-Trecate G, Morari M. Stability and stabilization of piecewise affine and hybrid systems: an lmi approach. In: Proceedings of the 39th IEEE conference on Decision and control, vol. 1; 2000. p. 504\u20139.","DOI":"10.1109\/CDC.2000.912814"},{"key":"10.1016\/j.cl.2015.12.002_bib21","doi-asserted-by":"crossref","unstructured":"Min\u00e9 A. A new numerical abstract domain based on difference-bound matrices. In: Programs as data objects, Second symposium, PADO 2001, Aarhus, Denmark; May 21\u201323, 2001. p. 155\u201372.","DOI":"10.1007\/3-540-44978-7_10"},{"issue":"1","key":"10.1016\/j.cl.2015.12.002_bib22","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","article-title":"The octagon abstract domain","volume":"19","author":"Min\u00e9","year":"2006","journal-title":"Higher-Order Symbol Comput"},{"issue":"0","key":"10.1016\/j.cl.2015.12.002_bib23","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1016\/0024-3795(81)90276-7","article-title":"Copositive matrices and definiteness of quadratic forms subject to homogeneous linear inequality constraints","volume":"35","author":"Martin","year":"1981","journal-title":"Linear Algebra Appl"},{"issue":"2","key":"10.1016\/j.cl.2015.12.002_bib24","doi-asserted-by":"crossref","first-page":"184","DOI":"10.2307\/1905733","article-title":"Two consequences of the transposition theorem on linear inequalities","volume":"19","author":"Motzkin","year":"1951","journal-title":"Econometrica"},{"key":"10.1016\/j.cl.2015.12.002_bib25","unstructured":"Prabhakar Pavithra, Viswanathan Mahesh. On the decidability of stability of hybrid systems. In: Belta Calin, Ivancic Franjo, editors. Proceedings of the 16th international conference on hybrid systems: computation and control, HSCC 2013, April 8\u201311, 2013, Philadelphia, PA, USA. ACM; 2013. p. 53\u201362."},{"key":"10.1016\/j.cl.2015.12.002_bib26","first-page":"240","article-title":"Integrating policy iterations in abstract interpreters","volume":"vol. 8172","author":"Roux","year":"2013"},{"issue":"April (4)","key":"10.1016\/j.cl.2015.12.002_bib27","doi-asserted-by":"crossref","first-page":"629","DOI":"10.1109\/9.847100","article-title":"Piecewise linear quadratic optimal control","volume":"45","author":"Rantzer","year":"2000","journal-title":"IEEE Trans. Automat. Control"},{"key":"10.1016\/j.cl.2015.12.002_bib28","series-title":"HSCC","first-page":"105","article-title":"A generic ellipsoid abstract domain for linear time invariant systems","author":"Roux","year":"2012"},{"key":"10.1016\/j.cl.2015.12.002_bib29","doi-asserted-by":"crossref","unstructured":"Sheeran M, Singh S, St\u00e5lmarck G. Checking safety properties using induction and a sat-solver. In: Hunt Jr WA, Johnson SD, editors. Formal methods in computer-aided design, third international conference, FMCAD 2000, Austin, TX, USA, November 1\u20133, 2000, Proceedings. Lecture notes in computer science, vol. 1954. Springer; 2000. p. 108\u201325.","DOI":"10.1007\/3-540-40922-X_8"}],"container-title":["Computer Languages, Systems & Structures"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1477842415000937?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1477842415000937?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2018,9,16]],"date-time":"2018-09-16T17:27:50Z","timestamp":1537118870000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1477842415000937"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,1]]},"references-count":29,"alternative-id":["S1477842415000937"],"URL":"https:\/\/doi.org\/10.1016\/j.cl.2015.12.002","relation":{},"ISSN":["1477-8424"],"issn-type":[{"value":"1477-8424","type":"print"}],"subject":[],"published":{"date-parts":[[2017,1]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Automatic synthesis of k-inductive piecewise quadratic invariants for switched affine control programs","name":"articletitle","label":"Article Title"},{"value":"Computer Languages, Systems & Structures","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.cl.2015.12.002","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2015 Elsevier Ltd. All rights reserved.","name":"copyright","label":"Copyright"}]}}