{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T16:06:20Z","timestamp":1770221180417,"version":"3.49.0"},"reference-count":99,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"3","license":[{"start":{"date-parts":[[2013,3,1]],"date-time":"2013-03-01T00:00:00Z","timestamp":1362096000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Automat. Contr."],"published-print":{"date-parts":[[2013,3]]},"DOI":"10.1109\/tac.2013.2241472","type":"journal-article","created":{"date-parts":[[2013,1,21]],"date-time":"2013-01-21T19:09:23Z","timestamp":1358795363000},"page":"696-711","source":"Crossref","is-referenced-by-count":15,"title":["Optimization of Lyapunov Invariants in Verification of Software Systems"],"prefix":"10.1109","volume":"58","author":[{"given":"M.","family":"Roozbehani","sequence":"first","affiliation":[]},{"given":"A.","family":"Megretski","sequence":"additional","affiliation":[]},{"given":"E.","family":"Feron","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1049\/ip-d.1982.0053"},{"key":"ref38","first-page":"620","article-title":"The solution of certain matrix inequalities in automatic control theory","volume":"3","author":"yakubovich","year":"1962","journal-title":"Soviet Math Dokl"},{"key":"ref33","author":"hecht","year":"1977","journal-title":"Flow Analysis of Computer Programs"},{"key":"ref32","author":"pierce","year":"2002","journal-title":"Types and Programming Languages"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24725-8_4"},{"key":"ref30","first-page":"215","volume":"3576","author":"costan","year":"2005","journal-title":"Computer-Aided Verification 90"},{"key":"ref37","volume":"17","author":"lyapunov","year":"1947","journal-title":"Probl\ufffdme G\ufffdn\ufffdral de la Stabilit\ufffd du Mouvement"},{"key":"ref36","author":"kailath","year":"1980","journal-title":"Linear Systems"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1145\/1965724.1965743"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375616"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-47764-0_14"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.2514\/6.2010-3385"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1145\/996841.996869"},{"key":"ref20","author":"dams","year":"1996","journal-title":"Abstract Interpretation and Partition Refinement for Model Checking"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_56"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45873-5_36"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44577-3_10"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"ref26","year":"2012"},{"key":"ref25","author":"adje","year":"2011","journal-title":"Optimisation et Jeux Appliqus l'analyse Statique de Programmes par Interprtation Abstraite"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1007\/11730637_22"},{"key":"ref51","first-page":"186","volume":"1567","author":"lafferriere","year":"1999","journal-title":"Hybrid Syst"},{"key":"ref59","author":"bertsimas","year":"1997","journal-title":"Introduction to Linear Optimization"},{"key":"ref58","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_1"},{"key":"ref57","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2006.377333"},{"key":"ref56","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31954-2_39"},{"key":"ref55","doi-asserted-by":"publisher","DOI":"10.1109\/ACC.2005.1470160"},{"key":"ref54","author":"feron","year":"2004","journal-title":"Abstraction Mechanisms Across the Board A Short Introduction"},{"key":"ref53","doi-asserted-by":"publisher","DOI":"10.1137\/050645178"},{"key":"ref52","author":"khalil","year":"2002","journal-title":"Nonlinear Systems"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1109\/9.863598"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3540-6"},{"key":"ref3","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1109\/MCS.2003.1172827","article-title":"Software technology for implementing reusable, distributed control systems","volume":"23","author":"heck","year":"2003","journal-title":"IEEE Control Syst Mag"},{"key":"ref6","author":"monin","year":"2003","journal-title":"Understanding Formal Methods"},{"key":"ref5","author":"nielson","year":"2004","journal-title":"Principles of Program Analysis"},{"key":"ref8","author":"hopcroft","year":"2006","journal-title":"Introduction to Automata Theory Languages and Computation"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1109\/9.664157"},{"key":"ref7","author":"clarke","year":"1999","journal-title":"Model checking"},{"key":"ref9","author":"kaynar","year":"2010","journal-title":"The Theory of Timed I\/O Automata"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46430-1_8"},{"key":"ref45","author":"kurzhanski","year":"1996","journal-title":"Ellipsoidal Calculus for Estimation and Control"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1109\/9.664150"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2007.902736"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2009.2034922"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.03.045"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.2001.0472"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2005.1582904"},{"key":"ref73","doi-asserted-by":"publisher","DOI":"10.1109\/9.587335"},{"key":"ref72","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_20"},{"key":"ref71","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134029"},{"key":"ref70","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177725"},{"key":"ref76","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2008.4739402"},{"key":"ref77","author":"gahinet","year":"1994","journal-title":"A Package for manipulating and Solving LMIs"},{"key":"ref74","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542518"},{"key":"ref75","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78929-1_32"},{"key":"ref78","doi-asserted-by":"publisher","DOI":"10.1080\/10556789908805766"},{"key":"ref79","year":"0","journal-title":"IBM ILOG CPLEX Optimization Studio"},{"key":"ref60","doi-asserted-by":"publisher","DOI":"10.1137\/1038003"},{"key":"ref62","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-09686-5_7"},{"key":"ref61","doi-asserted-by":"publisher","DOI":"10.1142\/ICPOS"},{"key":"ref63","doi-asserted-by":"publisher","DOI":"10.1007\/s10107-003-0387-5"},{"key":"ref64","author":"roozbehani","year":"2011","journal-title":"?Optimization of Lyapunov Invariants in Analysis of Software Systems ?"},{"key":"ref65","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24725-8_2"},{"key":"ref66","doi-asserted-by":"publisher","DOI":"10.1002\/9781118627372"},{"key":"ref67","doi-asserted-by":"publisher","DOI":"10.1016\/S0005-1098(98)00178-2"},{"key":"ref68","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00202-T"},{"key":"ref2","author":"murthy","year":"2001","journal-title":"Resource Management in Real-Time Systems and Networks"},{"key":"ref69","author":"brockett","year":"1993","journal-title":"Essays on Control Perspectives in the Theory and its Applicat"},{"key":"ref1","author":"kopetz","year":"2001","journal-title":"Real-Time Systems Design Principles for Distributed Embedded Applications"},{"key":"ref95","doi-asserted-by":"publisher","DOI":"10.1016\/0166-218X(92)00190-W"},{"key":"ref94","doi-asserted-by":"publisher","DOI":"10.1145\/227683.227684"},{"key":"ref93","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2009.2015979"},{"key":"ref92","doi-asserted-by":"crossref","DOI":"10.1007\/b96977","volume":"312","author":"henrion","year":"2005","journal-title":"Positive Polynomials in Control"},{"key":"ref91","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2003.1271743"},{"key":"ref90","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2002.1184595"},{"key":"ref98","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2006.882933"},{"key":"ref99","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1109\/TAC.2007.911318","article-title":"A passivity-based approach to stability of spatially distributed systems with a cyclic interconnection structure","volume":"53","author":"jovanovic","year":"2008","journal-title":"IEEE Trans Autom Control"},{"key":"ref96","year":"2012"},{"key":"ref97","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2012.2190163"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/BF01383968"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.21236\/ADA327281"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1145\/239098.239114"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2003.1205180"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"ref82","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-4381-7_13"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379017"},{"key":"ref81","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-0348-8362-7_15"},{"key":"ref18","first-page":"337","volume":"4963","author":"de moura","year":"2008","journal-title":"Tools and Algorithms for the Construction and Anal of Syst"},{"key":"ref84","author":"parrilo","year":"2000","journal-title":"Structured Semidefinite Programs and Semialgebraic Geometry Methods in Robustness and Optimization"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1145\/1132357.1132363"},{"key":"ref83","first-page":"73","article-title":"<formula formulatype=\"inline\"> <tex Notation=\"TeX\">${\\rm S}$<\/tex><\/formula>-procedure in nonlinear control theory","volume":"4","author":"yakubovich","year":"1977","journal-title":"Vestnik Leningrad Univ"},{"key":"ref80","doi-asserted-by":"publisher","DOI":"10.1137\/0801013"},{"key":"ref89","doi-asserted-by":"publisher","DOI":"10.1145\/1377612.1377619"},{"key":"ref85","doi-asserted-by":"publisher","DOI":"10.1134\/S000511790611004X"},{"key":"ref86","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-03718-8"},{"key":"ref87","author":"prajna","year":"2004","journal-title":"SOSTOOLS Sum of squares optimization toolbox for Matlab"},{"key":"ref88","first-page":"284","article-title":"YALMIP : A toolbox for modeling and optimization in MATLAB","author":"l\ufffdfberg","year":"2004","journal-title":"Proc CACSD Conf"}],"container-title":["IEEE Transactions on Automatic Control"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/9\/6464594\/06416001.pdf?arnumber=6416001","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,23]],"date-time":"2021-12-23T18:14:37Z","timestamp":1640283277000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6416001\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,3]]},"references-count":99,"journal-issue":{"issue":"3"},"URL":"https:\/\/doi.org\/10.1109\/tac.2013.2241472","relation":{},"ISSN":["0018-9286","1558-2523"],"issn-type":[{"value":"0018-9286","type":"print"},{"value":"1558-2523","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,3]]}}}