{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:27:05Z","timestamp":1742912825465,"version":"3.40.3"},"publisher-location":"Cham","reference-count":41,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319216676"},{"type":"electronic","value":"9783319216683"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-21668-3_20","type":"book-chapter","created":{"date-parts":[[2015,7,13]],"date-time":"2015-07-13T15:08:53Z","timestamp":1436800133000},"page":"338-355","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Automatic Verification of Stability and Safety for Delay Differential Equations"],"prefix":"10.1007","author":[{"given":"Liang","family":"Zou","sequence":"first","affiliation":[]},{"given":"Martin","family":"Fr\u00e4nzle","sequence":"additional","affiliation":[]},{"given":"Naijun","family":"Zhan","sequence":"additional","affiliation":[]},{"given":"Peter Nazier","family":"Mosaad","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,14]]},"reference":[{"key":"20_CR1","volume-title":"Delay Differential Equations","author":"B Balachandran","year":"2009","unstructured":"Balachandran, B., Kalm\u00e1r-Nagy, T., Gilsinn, D.E.: Delay Differential Equations. Springer, (2009)"},{"key":"20_CR2","unstructured":"Richard, B., Cooke, K.L.: Differential-difference equations. Technical report R-374-PR, The RAND Corporation, Santa Monica (1963)"},{"issue":"4","key":"20_CR3","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1023\/A:1024467732637","volume":"4","author":"M Berz","year":"1998","unstructured":"Berz, M., Makino, K.: Verified integration of ODEs and flows using differential algebraic methods on high-order Taylor models. Reliable Comput. 4(4), 361\u2013369 (1998)","journal-title":"Reliable Comput."},{"key":"20_CR4","first-page":"215","volume":"15","author":"B Stephen","year":"1994","unstructured":"Stephen, B., El Ghaoui, L., Feron, E., Balakrishnan, V.: Linear matrix inequalities in system and control theory of studies in applied mathematics. Soc. Ind. Appl. Math. (SIAM) 15, 215\u2013249 (1994)","journal-title":"Soc. Ind. Appl. Math. (SIAM)"},{"key":"20_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-642-39799-8_18","volume-title":"Computer Aided Verification","author":"X Chen","year":"2013","unstructured":"Chen, X., \u00c1brah\u00e1m, E., Sankaranarayanan, S.: Flow*: an analyzer for non-linear hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 258\u2013263. Springer, Heidelberg (2013)"},{"key":"20_CR6","unstructured":"Chutinan, A., Krogh, B.H.: Computing polyhedral approximations to flow pipes for dynamic systems. In: Proceedings of the 37th International Conference on Decision and Control (CDC 1998) (1998)"},{"issue":"5","key":"20_CR7","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1016\/S0167-6911(01)00118-9","volume":"43","author":"J Daafouz","year":"2001","unstructured":"Daafouz, J., Bernussou, J.: Parameter dependent Lyapunov functions for discrete time systems with time varying parametric uncertainties. Sys. Control Lett. 43(5), 355\u2013359 (2001)","journal-title":"Sys. Control Lett."},{"key":"20_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-540-88387-6_14","volume-title":"Automated Technology for Verification and Analysis","author":"A Eggers","year":"2008","unstructured":"Eggers, A., Fr\u00e4nzle, M., Herde, C.: SAT Modulo ODE: a direct SAT approach to hybrid systems. In: Cha, S.S., Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 171\u2013185. Springer, Heidelberg (2008)"},{"key":"20_CR9","first-page":"1","volume":"6","author":"E Andreas","year":"2012","unstructured":"Andreas, E., Nacim, R., Nedialkov, N.S., Fr\u00e4nzle, M.: Improving the SAT modulo ODE approach to hybrid systems analysis by combining different enclosure methods. Software Systems Modeling 6, 1\u201328 (2012)","journal-title":"Software Systems Modeling"},{"issue":"4","key":"20_CR10","doi-asserted-by":"publisher","first-page":"867","DOI":"10.1103\/PhysRevLett.82.867","volume":"82","author":"J Fort","year":"1999","unstructured":"Fort, J., M\u00e9ndez, V.: Time-delayed theory of the neolithic transition in europe. Phys. Rev. Lett 82(4), 867 (1999)","journal-title":"Phys. Rev. Lett"},{"key":"20_CR11","first-page":"209","volume":"1","author":"M Fr\u00e4nzle","year":"2007","unstructured":"Fr\u00e4nzle, M., Herde, C., Ratschan, S., Schubert, T., Teige, T.: Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure. J. Satisfiability Boolean Model. Comput. Spec. Issue SAT\/CP Integr. 1, 209\u2013236 (2007)","journal-title":"J. Satisfiability Boolean Model. Comput. Spec. Issue SAT\/CP Integr."},{"key":"20_CR12","doi-asserted-by":"publisher","first-page":"436","DOI":"10.1016\/j.jlap.2010.07.003","volume":"79","author":"M Fr\u00e4nzle","year":"2010","unstructured":"Fr\u00e4nzle, M., Teige, T., Eggers, A.: Engineering constraint solvers for automatic analysis of probabilistic hybrid automata. J. Logic Algebraic Programm. 79, 436\u2013466 (2010)","journal-title":"J. Logic Algebraic Programm."},{"key":"20_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/978-3-540-31954-2_19","volume-title":"Hybrid Systems: Computation and Control","author":"A Girard","year":"2005","unstructured":"Girard, A.: Reachability of uncertain linear systems using zonotopes. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 291\u2013305. Springer, Heidelberg (2005)"},{"key":"20_CR14","doi-asserted-by":"crossref","DOI":"10.1515\/9780691221793","volume-title":"From Clocks to Chaos: The Rhythms of Life","author":"L Glass","year":"1988","unstructured":"Glass, L., Mackey, M.C.: From Clocks to Chaos: The Rhythms of Life. Princeton University Press, Princeton (1988)"},{"key":"20_CR15","unstructured":"Gustafson, G.B.: Systems of differential equations. In: Manuscript for Course Eng Math 2250\u20131 Spring 2014, ch 11. University of Utah, Department of Mathematics (2014)"},{"issue":"1","key":"20_CR16","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1006\/jcss.1998.1581","volume":"57","author":"TA Henzinger","year":"1998","unstructured":"Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What\u2019s decidable about hybrid automata? J. Comput. Syst. Sci. 57(1), 94\u2013124 (1998)","journal-title":"J. Comput. Syst. Sci."},{"issue":"1\u20132","key":"20_CR17","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1016\/0167-2789(87)90058-3","volume":"29","author":"K Ikeda","year":"1987","unstructured":"Ikeda, K., Matsumoto, K.: High-dimensional chaotic behavior in systems with time-delayed feedback. Physica D 29(1\u20132), 223\u2013235 (1987)","journal-title":"Physica D"},{"key":"20_CR18","doi-asserted-by":"crossref","unstructured":"Kong, S., Gao, S., Chen, W., Clarke, E.: dReach: delta-reachability analysis for hybrid systems. In: TACAS (2015)","DOI":"10.1007\/978-3-662-46681-0_15"},{"key":"20_CR19","series-title":"Lecture Notes in Control and Information Sciences","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/10984413_12","volume-title":"New Directions and Applications in Control Theory","author":"AB Kurzhanski","year":"2005","unstructured":"Kurzhanski, A.B., Varaiya, P.: Ellipsoidal techniques for hybrid dynamics: the reachability problem. In: Dayawansa, W.P., Lindquist, A., Zhou, Y. (eds.) New Directions and Applications in Control Theory. Lecture Notes in Control and Information Sciences, pp. 193\u2013205. Springer, Heidelberg (2005)"},{"issue":"3","key":"20_CR20","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1006\/jsco.2001.0472","volume":"32","author":"G Lafferriere","year":"2001","unstructured":"Lafferriere, G., Pappas, G.J., Yovine, S.: Symbolic reachability computation for families of linear vector fields. J. Symbolic Comput. 32(3), 231\u2013253 (2001)","journal-title":"J. Symbolic Comput."},{"key":"20_CR21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14938-2","volume-title":"Dynamics of Nonlinear Time-delay Systems. Springer Science Business Media","author":"M Lakshmanan","year":"2011","unstructured":"Lakshmanan, M., Senthilkumar, D.V.: Dynamics of Nonlinear Time-delay Systems. Springer Science Business Media. Springer, Heidelberg (2011)"},{"issue":"2","key":"20_CR22","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1016\/j.nahs.2009.03.002","volume":"4","author":"C Guernic Le","year":"2010","unstructured":"Le Guernic, C., Girard, A.: Reachability analysis of linear systems using support functions. Nonlinear Anal. Hybrid Sys. 4(2), 250\u2013262 (2010)","journal-title":"Nonlinear Anal. Hybrid Sys."},{"key":"20_CR23","doi-asserted-by":"crossref","unstructured":"Liu, J., Zhan, N., Zhao, H.: Computing semi-algebraic invariants for polynomial dynamical systems. In: EMSOFT 2011, pp. 97\u2013106. ACM New York (2011)","DOI":"10.1145\/2038642.2038659"},{"issue":"4","key":"20_CR24","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/s11786-012-0133-6","volume":"6","author":"J Liu","year":"2012","unstructured":"Liu, J., Zhan, N., Zhao, H.: Automatically discovering relaxed Lyapunov functions for polynomial dynamical systems. Math. Comput. Sci. 6(4), 395\u2013408 (2012)","journal-title":"Math. Comput. Sci."},{"key":"20_CR25","unstructured":"Lohner, R.: Einschlie\u00dfung der L\u00f6sung gew\u00f6hnlicher Anfangs- und Randwertaufgaben. Ph.D. thesis, Fakult\u00e4t f\u00fcr Mathematik der Universit\u00e4t Karlsruhe, Karlsruhe (1988)"},{"issue":"4300","key":"20_CR26","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1126\/science.267326","volume":"197","author":"MC Mackey","year":"1977","unstructured":"Mackey, M.C., Glass, L., et al.: Oscillation and chaos in physiological control systems. Science 197(4300), 287\u2013289 (1977)","journal-title":"Science"},{"key":"20_CR27","series-title":"volume II","first-page":"103","volume-title":"Error in Digital Computation","author":"RE Moore","year":"1965","unstructured":"Moore, R.E.: Automatic local coordinate transformation to reduce the growth of error bounds in interval computation of solutions of ordinary differential equations. In: Ball, L.B. (ed.) Error in Digital Computation. volume II, pp. 103\u2013140. Wiley, New York (1965)"},{"issue":"1","key":"20_CR28","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1137\/050638448","volume":"45","author":"M Neher","year":"2007","unstructured":"Neher, M., Jackson, K.R., Nedialkov, N.S.: On Taylor model based integration of ODEs. SIAM J. Numer. Anal. 45(1), 236\u2013262 (2007)","journal-title":"SIAM J. Numer. Anal."},{"key":"20_CR29","unstructured":"Oehlerking, J.: Decomposition of Stability Proofs for Hybrid Systems. Doctoral dissertation, Carl von Ossietzky Universit\u00e4t Oldenburg, Department of Computing Science (2011)"},{"issue":"1","key":"20_CR30","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1093\/logcom\/exn070","volume":"20","author":"A Platzer","year":"2010","unstructured":"Platzer, A.: Differential-algebraic dynamic logic for differential-algebraic programs. J. Log. Comput. 20(1), 309\u2013352 (2010)","journal-title":"J. Log. Comput."},{"key":"20_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/978-3-540-70545-1_17","volume-title":"Computer Aided Verification","author":"A Platzer","year":"2008","unstructured":"Platzer, A., Clarke, E.M.: Computing differential invariants of hybrid systems as fixedpoints. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 176\u2013189. Springer, Heidelberg (2008)"},{"issue":"8","key":"20_CR32","doi-asserted-by":"publisher","first-page":"1415","DOI":"10.1109\/TAC.2007.902736","volume":"52","author":"S Prajna","year":"2007","unstructured":"Prajna, S., Jadbabaie, A., Pappas, G.J.: A framework for worst-case and stochastic safety verification using barrier certificates. IEEE Trans. Autom. Control 52(8), 1415\u20131428 (2007)","journal-title":"IEEE Trans. Autom. Control"},{"key":"20_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/978-3-540-31954-2_37","volume-title":"Hybrid Systems: Computation and Control","author":"S Ratschan","year":"2005","unstructured":"Ratschan, S., She, Z.: Safety verification of hybrid systems by constraint propagation based abstraction refinement. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 573\u2013589. Springer, Heidelberg (2005)"},{"key":"20_CR34","doi-asserted-by":"crossref","unstructured":"Ratschan, S., She, Z.: Providing a basin of attraction to a target region by computation of Lyapunov-like functions. In: IEEE International Conference on Computational Cybernetics (ICCC 2006), pp. 1\u20135 (2006)","DOI":"10.1109\/ICCCYB.2006.305705"},{"issue":"1\u20132","key":"20_CR35","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1080\/03081089508818341","volume":"38","author":"J Rohn","year":"1994","unstructured":"Rohn, J., Kreslov\u00e1, J.: Linear interval inequalities. Linear Multilinear Algebra 38(1\u20132), 79\u201382 (1994)","journal-title":"Linear Multilinear Algebra"},{"key":"20_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"539","DOI":"10.1007\/978-3-540-24743-2_36","volume-title":"Hybrid Systems: Computation and Control","author":"S Sankaranarayanan","year":"2004","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constructing invariants for hybrid systems. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 539\u2013554. Springer, Heidelberg (2004)"},{"key":"20_CR37","unstructured":"Stauning, O.: Automatic Validation of Numerical Solutions. Ph.D .thesis, Technical University of Denmark, Lyngby (1997)"},{"issue":"2","key":"20_CR38","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1016\/j.chaos.2004.11.012","volume":"25","author":"M Szyd\u0142owski","year":"2005","unstructured":"Szyd\u0142owski, M., Krawiec, A.: The stability problem in the kaldor-kalecki business cycle model. Chaos Solitons Fractals 25(2), 299\u2013305 (2005)","journal-title":"Chaos Solitons Fractals"},{"issue":"3","key":"20_CR39","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1016\/S0960-0779(99)00207-6","volume":"12","author":"M Szyd\u0142owski","year":"2001","unstructured":"Szyd\u0142owski, M., Krawiec, A., Tobo\u0142a, J.: Nonlinear oscillations in business cycle model with time lags. Chaos, Solitons Fractals 12(3), 505\u2013517 (2001)","journal-title":"Chaos, Solitons Fractals"},{"key":"20_CR40","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1017\/S0013091506000988","volume":"51","author":"X Tang","year":"2008","unstructured":"Tang, X., Zou, X.: Global attractivity in a predator-prey system with pure delays. Proc. Edinburgh Math. Soc. 51, 495\u2013508 (2008)","journal-title":"Proc. Edinburgh Math. Soc."},{"key":"20_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/978-3-642-54108-7_14","volume-title":"Verified Software: Theories, Tools, Experiments","author":"L Zou","year":"2014","unstructured":"Zou, L., Lv, J., Wang, S., Zhan, N., Tang, T., Yuan, L., Liu, Y.: Verifying chinese train control system under a combined scenario by theorem proving. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol. 8164, pp. 262\u2013280. Springer, Heidelberg (2014)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21668-3_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,18]],"date-time":"2022-05-18T00:51:30Z","timestamp":1652835090000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-21668-3_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319216676","9783319216683"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21668-3_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"14 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}