{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,4]],"date-time":"2026-04-04T06:14:31Z","timestamp":1775283271355,"version":"3.50.1"},"reference-count":80,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2018,11,24]],"date-time":"2018-11-24T00:00:00Z","timestamp":1543017600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2018,11,24]],"date-time":"2018-11-24T00:00:00Z","timestamp":1543017600000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"crossref","award":["EP\/I010335\/1"],"award-info":[{"award-number":["EP\/I010335\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"crossref","award":["EP\/J001058\/1"],"award-info":[{"award-number":["EP\/J001058\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100000083","name":"Directorate for Computer and Information Science and Engineering","doi-asserted-by":"publisher","award":["CNS 1464311"],"award-info":[{"award-number":["CNS 1464311"]}],"id":[{"id":"10.13039\/100000083","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF 1527398"],"award-info":[{"award-number":["CCF 1527398"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006602","name":"Air Force Research Laboratory","doi-asserted-by":"publisher","award":["FA8750-15-1-0105"],"award-info":[{"award-number":["FA8750-15-1-0105"]}],"id":[{"id":"10.13039\/100006602","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["FA9550-15-1-0258"],"award-info":[{"award-number":["FA9550-15-1-0258"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2019,12]]},"DOI":"10.1007\/s10817-018-9497-x","type":"journal-article","created":{"date-parts":[[2018,11,24]],"date-time":"2018-11-24T09:43:14Z","timestamp":1543052594000},"page":"1005-1029","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Verifying Safety and Persistence in Hybrid Systems Using Flowpipes and Continuous Invariants"],"prefix":"10.1007","volume":"63","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5849-7991","authenticated-orcid":false,"given":"Andrew","family":"Sogokon","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3863-8336","authenticated-orcid":false,"given":"Paul B.","family":"Jackson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8021-9923","authenticated-orcid":false,"given":"Taylor T.","family":"Johnson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,11,24]]},"reference":[{"issue":"3","key":"9497_CR1","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/s10817-009-9149-2","volume":"44","author":"B Akbarpour","year":"2010","unstructured":"Akbarpour, B., Paulson, L.C.: MetiTarski: an automatic theorem prover for real-valued special functions. J. Autom. Reason. 44(3), 175\u2013205 (2010)","journal-title":"J. Autom. Reason."},{"key":"9497_CR2","first-page":"209","volume-title":"Hybrid Systems, Volume 736 of LNCS","author":"R Alur","year":"1992","unstructured":"Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.: Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.) Hybrid Systems, Volume 736 of LNCS, pp. 209\u2013229. Springer, Berlin (1992)"},{"key":"9497_CR3","series-title":"Lecture Notes in Computer Science","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","year":"2015","unstructured":"Baier, C., Tinelli, C. (eds.): Tools and Algorithms for the Construction and Analysis of Systems\u201421st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11\u201318, 2015. Proceedings, volume 9035 of LNCS. Springer (2015)"},{"key":"9497_CR4","doi-asserted-by":"crossref","unstructured":"Bemporad, A., Bicchi, A., Buttazzo, G.C. (eds.): Hybrid Systems: Computation and Control, 10th International Workshop, HSCC 2007, Pisa, Italy, April 3\u20135, 2007, Proceedings, Volume 4416 of LNCS. Springer (2007)","DOI":"10.1007\/978-3-540-71493-4"},{"issue":"4","key":"9497_CR5","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. Reliab. Comput. 4(4), 361\u2013369 (1998)","journal-title":"Reliab. Comput."},{"issue":"11","key":"9497_CR6","doi-asserted-by":"publisher","first-page":"1747","DOI":"10.1016\/S0005-1098(99)00113-2","volume":"35","author":"F Blanchini","year":"1999","unstructured":"Blanchini, F.: Set invariance in control. Automatica 35(11), 1747\u20131767 (1999)","journal-title":"Automatica"},{"key":"9497_CR7","unstructured":"Carter, R.A:. Verification of liveness properties on hybrid dynamical systems. Ph.D. thesis, University of Manchester, School of Computer Science (2013)"},{"key":"9497_CR8","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-642-39799-8_18","volume-title":"Computer Aided Verification","author":"Xin Chen","year":"2013","unstructured":"Chen, X., \u00c1brah\u00e1m, E., Sankaranarayanan, S.: Flow*: an analyzer for non-linear hybrid systems. In: Sharygina and Veith [69], pp. 258\u2013263"},{"issue":"4","key":"9497_CR9","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1142\/S012905410300190X","volume":"14","author":"EM Clarke","year":"2003","unstructured":"Clarke, E.M., Fehnker, A., Han, Z., Krogh, B.H., Ouaknine, J., Stursberg, O., Theobald, M.: Abstraction and counterexample-guided refinement in model checking of hybrid systems. Int. J. Found. Comput. Sci. 14(4), 583\u2013604 (2003)","journal-title":"Int. J. Found. Comput. Sci."},{"issue":"1","key":"9497_CR10","first-page":"1","volume":"8","author":"C Cohen","year":"2012","unstructured":"Cohen, C., Mahboubi, A.: Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination. Log. Methods Comput. Sci. 8(1), 1\u201340 (2012)","journal-title":"Log. Methods Comput. Sci."},{"key":"9497_CR11","doi-asserted-by":"crossref","unstructured":"Collins, G.E.: Hauptvortrag: quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Barkhage, H. (ed.) Automata Theory and Formal Languages, 2nd GI Conference, Kaiserslautern, May 20\u201323, 1975, Volume 33 of LNCS, pp. 134\u2013183. Springer, Berlin (1975)","DOI":"10.1007\/3-540-07407-4_17"},{"key":"9497_CR12","doi-asserted-by":"crossref","unstructured":"Davenport, J.H., England, M.: Recent advances in real geometric reasoning. In: Botana, F., Quaresma, P. (eds.) Automated Deduction in Geometry\u201410th International Workshop, ADG 2014, Coimbra, Portugal, July 9\u201311, 2014, Revised Selected Papers, Volume 9201 of LNCS, pp. 37\u201352. Springer (2014)","DOI":"10.1007\/978-3-319-21362-0_3"},{"issue":"5","key":"9497_CR13","doi-asserted-by":"publisher","first-page":"627","DOI":"10.1016\/0005-1098(71)90027-6","volume":"7","author":"E Davison","year":"1971","unstructured":"Davison, E., Kurak, E.: A computational method for determining quadratic Lyapunov functions for non-linear systems. Automatica 7(5), 627\u2013636 (1971)","journal-title":"Automatica"},{"key":"9497_CR14","doi-asserted-by":"crossref","unstructured":"Donz\u00e9, A., Maler, O.: Systematic simulation using sensitivity analysis. In: Bemporad et\u00a0al. [4], pp. 174\u2013189","DOI":"10.1007\/978-3-540-71493-4_16"},{"key":"9497_CR15","unstructured":"Duggirala, P.S., Mitra, S.: Abstraction refinement for stability. In: 2011 IEEE\/ACM International Conference on Cyber-Physical Systems, ICCPS 2011, Chicago, Illinois, USA, 12\u201314 April, 2011, pp. 22\u201331. IEEE Computer Society (2011)"},{"key":"9497_CR16","unstructured":"Duggirala, P.S., Mitra, S.: Lyapunov abstractions for inevitability of hybrid systems. In: Dang, T., Mitchell, I.M. (eds.) Hybrid Systems: Computation and Control (Part of CPS Week 2012), HSCC\u201912, Beijing, China, April 17\u201319, 2012, pp. 115\u2013124. ACM (2012)"},{"issue":"1","key":"9497_CR17","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/s10270-012-0295-3","volume":"14","author":"A Eggers","year":"2015","unstructured":"Eggers, A., Ramdani, N., Nedialkov, N.S., Fr\u00e4nzle, M.: Improving the SAT modulo ODE approach to hybrid systems analysis by combining different enclosure methods. Softw. Syst. Model. 14(1), 121\u2013148 (2015)","journal-title":"Softw. Syst. Model."},{"key":"9497_CR18","unstructured":"Fan, C., Kapinski, J., Jin, X., Mitra, S.: Locally optimal reach set over-approximation for nonlinear systems. In: 2016 International Conference on Embedded Software, EMSOFT 2016, Pittsburgh, Pennsylvania, USA, October 1\u20137, 2016, pp. 6:1\u20136:10. ACM (2016)"},{"key":"9497_CR19","first-page":"28","volume":"17(1):21:1\u201321","author":"C Fan","year":"2018","unstructured":"Fan, C., Kapinski, J., Jin, X., Mitra, S.: Simulation-driven reachability using matrix measures. ACM Trans. Embed. Comput. Syst. 17(1):21:1\u201321, 28 (2018)","journal-title":"ACM Trans. Embed. Comput. Syst."},{"key":"9497_CR20","doi-asserted-by":"crossref","unstructured":"Forsman, K.: Construction of Lyapunov functions using Gr\u00f6bner bases, Vol. 1, pp. 798\u2013799. IEEE(1991)","DOI":"10.1109\/CDC.1991.261424"},{"key":"9497_CR21","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/978-3-642-22110-1_30","volume-title":"Computer Aided Verification","author":"Goran Frehse","year":"2011","unstructured":"Frehse, G., Guernic, C.L., Donz\u00e9, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) Computer Aided Verification\u201423rd International Conference, CAV 2011, Snowbird, UT, USA, July 14\u201320, 2011. Proceedings, Volume 6806 of LNCS, pp. 379\u2013395. Springer (2011)"},{"key":"9497_CR22","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1007\/978-3-319-21401-6_36","volume-title":"Automated Deduction - CADE-25","author":"Nathan Fulton","year":"2015","unstructured":"Fulton, N., Mitsch, S., Quesel, J., V\u00f6lp, M., Platzer, A.: KeYmaera X: an axiomatic tactical theorem prover for hybrid systems. In: Felty, A.P., Middeldorp, A. (eds.) Automated Deduction\u2014CADE-25\u201425th International Conference on Automated Deduction, Berlin, Germany, August 1\u20137, 2015, Proceedings, Volume 9195 of LNCS, pp. 527\u2013538. Springer (2015)"},{"key":"9497_CR23","unstructured":"Ghorbal, K., Platzer, A.: Characterizing algebraic invariants by differential radical invariants. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) Tools and Algorithms for the Construction and Analysis of Systems\u201420th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5\u201313, 2014. Proceedings, Volume 8413 of LNCS, pp. 279\u2013294. Springer (2014)"},{"key":"9497_CR24","first-page":"19","volume":"47","author":"K Ghorbal","year":"2017","unstructured":"Ghorbal, K., Sogokon, A., Platzer, A.: A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets. Comput. Lang. Syst. Struct. 47, 19\u201343 (2017)","journal-title":"Comput. Lang. Syst. Struct."},{"key":"9497_CR25","unstructured":"Goubault, E., Jourdan, J., Putot, S., Sankaranarayanan, S.: Finding non-polynomial positive invariants and Lyapunov functions for polynomial systems through Darboux polynomials. In: American Control Conference, ACC 2014, Portland, OR, USA, June 4\u20136, 2014, pp. 3571\u20133578. IEEE (2014)"},{"key":"9497_CR26","unstructured":"Goubault, E., Putot, S.: Forward inner-approximated reachability of non-linear continuous systems. In: Frehse, G., Mitra, S. (eds.) Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control, HSCC 2017, Pittsburgh, PA, USA, April 18\u201320, 2017, pp. 1\u201310. ACM (2017)"},{"key":"9497_CR27","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Tiwari, A.: Constraint-based approach for analysis of hybrid systems. In: Gupta and Malik [28], pp. 190\u2013203","DOI":"10.1007\/978-3-540-70545-1_18"},{"key":"9497_CR28","doi-asserted-by":"crossref","unstructured":"Gupta, A., Malik, S. (eds.): Computer Aided Verification, 20th International Conference, CAV 2008, Princeton, NJ, USA, July 7\u201314, 2008, Proceedings, Volume 5123 of LNCS. Springer (2008)","DOI":"10.1007\/978-3-540-70545-1"},{"key":"9497_CR29","unstructured":"Henzinger, T.A.: The theory of hybrid automata. In: Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27\u201330, 1996, pp. 278\u2013292. IEEE Computer Society (1996)"},{"key":"9497_CR30","doi-asserted-by":"crossref","unstructured":"Immler, F.: Verified reachability analysis of continuous systems. In: Baier and Tinelli [3], pp. 37\u201351","DOI":"10.1007\/978-3-662-46681-0_3"},{"key":"9497_CR31","unstructured":"Jirstrand, M.: Cylindrical algebraic decomposition\u2014an introduction. Technical Report 1807, Link\u00f6ping University, Automatic Control (1995)"},{"key":"9497_CR32","unstructured":"Kapela, T., Mrozek, M., Pilarczyk, P., Wilczak, D., Zgliczy\u0144ski, P.: CAPD\u2014a rigorous toolbox for computer assisted proofs in dynamics. Technical report, Jagiellonian University, Krakow, Poland (2010). http:\/\/capd.ii.uj.edu.pl\/ . Accessed 20 Nov 2018"},{"key":"9497_CR33","volume-title":"Nonlinear Systems","author":"HK Khalil","year":"2002","unstructured":"Khalil, H.K.: Nonlinear Systems, 3rd edn. Prentice Hall, Upper Saddle River (2002)","edition":"3"},{"key":"9497_CR34","unstructured":"Kong, S., Gao, S., Chen, W., Clarke, E.M.: dreach: $${\\delta }$$-reachability analysis for hybrid systems. In: Baier and Tinelli [3], pp. 200\u2013205"},{"issue":"4","key":"9497_CR35","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/BF01995674","volume":"2","author":"R Koymans","year":"1990","unstructured":"Koymans, R.: Specifying real-time properties with metric temporal logic. Real Time Syst. 2(4), 255\u2013299 (1990)","journal-title":"Real Time Syst."},{"issue":"10","key":"9497_CR36","doi-asserted-by":"publisher","first-page":"1145","DOI":"10.1016\/j.apnum.2006.10.006","volume":"57","author":"Y Lin","year":"2007","unstructured":"Lin, Y., Stadtherr, M.A.: Validated solutions of initial value problems for parametric ODEs. Appl. Numer. Math. 57(10), 1145\u20131162 (2007)","journal-title":"Appl. Numer. Math."},{"key":"9497_CR37","unstructured":"Liu, J., Lv, J., Quan, Z., Zhan, N., Zhao, H., Zhou, C., Zou, L.: A calculus for hybrid CSP. In: Ueda, K. (ed) Programming Languages and Systems\u20148th Asian Symposium, APLAS 2010, Shanghai, China, November 28\u2013December 1, 2010. Proceedings, Volume 6461 of LNCS, pp. 1\u201315. Springer (2010)"},{"key":"9497_CR38","unstructured":"Liu, J., Zhan, N., Zhao, H.: Computing semi-algebraic invariants for polynomial dynamical systems. In: Chakraborty, S., Jerraya, A., Baruah, S.K., Fischmeister, S. (eds.) Proceedings of the 11th International Conference on Embedded Software, EMSOFT 2011, Part of the Seventh Embedded Systems Week, ESWeek 2011, Taipei, Taiwan, October 9\u201314, 2011, pp. 97\u2013106. ACM (2011)"},{"issue":"1","key":"9497_CR39","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1109\/TAC.2002.806650","volume":"48","author":"J Lygeros","year":"2003","unstructured":"Lygeros, J., Johansson, K.H., Simi\u0107, S.N., Zhang, J., Sastry, S.S.: Dynamical properties of hybrid automata. IEEE Trans. Autom. Control 48(1), 2\u201317 (2003)","journal-title":"IEEE Trans. Autom. Control"},{"key":"9497_CR40","unstructured":"Mahboubi, A.: Programming and certifying a CAD algorithm in the Coq system. In: Coquand, T., Lombardi, H., Roy, M. (eds.) Mathematics, Algorithms, Proofs, 9\u201314. January 2005, Volume 05021 of Dagstuhl Seminar Proceedings. Internationales Begegnungs- und Forschungszentrum f\u00fcr Informatik (IBFI), Schloss Dagstuhl, Germany (2005)"},{"key":"9497_CR41","unstructured":"Maidens, J.N., Arcak, M.: Trajectory-based reachability analysis of switched nonlinear systems using matrix measures. In: 53rd IEEE Conference on Decision and Control, CDC 2014, Los Angeles, CA, USA, December 15\u201317, 2014, pp. 6358\u20136364. IEEE (2014)"},{"issue":"1","key":"9497_CR42","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1109\/TAC.2014.2325635","volume":"60","author":"JN Maidens","year":"2015","unstructured":"Maidens, J.N., Arcak, M.: Reachability analysis of nonlinear systems using matrix measures. IEEE Trans. Autom. Control 60(1), 265\u2013270 (2015)","journal-title":"IEEE Trans. Autom. Control"},{"issue":"1","key":"9497_CR43","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1016\/j.nima.2005.11.109","volume":"558","author":"K Makino","year":"2006","unstructured":"Makino, K., Berz, M.: COSY INFINITY version 9. Nucl. Instrum. Methods Phys. Res. Sect. A 558(1), 346\u2013350 (2006)","journal-title":"Nucl. Instrum. Methods Phys. Res. Sect. A"},{"key":"9497_CR44","unstructured":"Manna, Z., Pnueli, A.: A hierarchy of temporal properties. In: Dwork, C. (ed) Proceedings of the Ninth Annual ACM Symposium on Principles of Distributed Computing, Quebec City, Quebec, Canada, August 22\u201324, 1990, pp. 377\u2013410. ACM (1990)"},{"key":"9497_CR45","unstructured":"Martin-Dorel, \u00c9., Roux, P.: A reflexive tactic for polynomial positivity using numerical solvers and floating-point computations. In: Bertot, Y., Vafeiadis, V. (eds.) Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16\u201317, 2017, pp. 90\u201399. ACM (2017)"},{"key":"9497_CR46","doi-asserted-by":"crossref","unstructured":"Mitrohin, C., Podelski, A.: Composing stability proofs for hybrid systems. In: Fahrenberg, U., Tripakis, S. (eds.) Formal Modeling and Analysis of Timed Systems\u20149th International Conference, FORMATS 2011, Aalborg, Denmark, September 21\u201323, 2011. Proceedings, Volume 6919 of LNCS, pp. 286\u2013300. Springer (2011)","DOI":"10.1007\/978-3-642-24310-3_20"},{"key":"9497_CR47","doi-asserted-by":"crossref","unstructured":"M\u00f6hlmann, E., Hagemann, W., Theel, O.E.: Hybrid tools for hybrid systems\u2014proving stability and safety at once. In: Sankaranarayanan, S., Vicario, E. (eds.) Formal Modeling and Analysis of Timed Systems\u201413th International Conference, FORMATS 2015, Madrid, Spain, September 2\u20134, 2015, Proceedings, Volume 9268 of LNCS, pp. 222\u2013239. Springer (2015)","DOI":"10.1007\/978-3-319-22975-1_15"},{"key":"9497_CR48","unstructured":"M\u00f6hlmann, E., Theel, O.E.: Stabhyli: a tool for automatic stability verification of non-linear hybrid systems. In: Belta, C., Ivan\u010di\u0107, F. (eds.) Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control, HSCC 2013, April 8\u201311, 2013, Philadelphia, PA, USA, pp. 107\u2013112. ACM (2013)"},{"issue":"11","key":"9497_CR49","doi-asserted-by":"publisher","first-page":"1883","DOI":"10.1080\/00207721.2010.495189","volume":"42","author":"EM Navarro-L\u00f3pez","year":"2011","unstructured":"Navarro-L\u00f3pez, E.M., Carter, R.: Hybrid automata: an insight into the discrete abstraction of discontinuous systems. Int. J. Syst. Sci. 42(11), 1883\u20131898 (2011)","journal-title":"Int. J. Syst. Sci."},{"issue":"C","key":"9497_CR50","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.tcs.2016.06.009","volume":"642","author":"EM Navarro-L\u00f3pez","year":"2016","unstructured":"Navarro-L\u00f3pez, E.M., Carter, R.: Deadness and how to disprove liveness in hybrid dynamical systems. Theor. Comput. Sci. 642(C), 1\u201323 (2016)","journal-title":"Theor. Comput. Sci."},{"key":"9497_CR51","doi-asserted-by":"crossref","unstructured":"Navarro-L\u00f3pez, E.M., Su\u00e1rez, R.: Practical approach to modelling and controlling stick-slip oscillations in oilwell drillstrings, Vol. 2, pp. 1454\u20131460. IEEE (2004)","DOI":"10.1109\/CCA.2004.1387580"},{"key":"9497_CR52","unstructured":"Nedialkov, N.S.: Interval tools for ODEs and DAEs. In: 12th GAMM\u2014IMACS International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics (SCAN 2006), Duisburg (2006)"},{"issue":"1","key":"9497_CR53","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":"9497_CR54","unstructured":"Nishida, T., Mizutani, K., Kubota, A., Doshita, S.: Automated phase portrait analysis by integrating qualitative and quantitative analysis. In: Dean, T.L., McKeown, K.R. (eds.) Proceedings of the 9th National Conference on Artificial Intelligence, Anaheim, CA, USA, July 14\u201319, 1991, Vol. 2, pp. 811\u2013816. AAAI Press\/The MIT Press (1991)"},{"key":"9497_CR55","first-page":"1","volume-title":"Interactive Theorem Proving","author":"Lawrence C. Paulson","year":"2012","unstructured":"Paulson, L.C.: MetiTarski: Past and future. In: Beringer, L., Felty, A.P. (eds.) Interactive Theorem Proving\u2014Third International Conference, ITP 2012, Princeton, NJ, USA, August 13\u201315, 2012. Proceedings, Volume 7406 of LNCS, pp. 1\u201310. Springer (2012)"},{"issue":"2","key":"9497_CR56","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/s10817-008-9103-8","volume":"41","author":"A Platzer","year":"2008","unstructured":"Platzer, A.: Differential dynamic logic for hybrid systems. J. Autom. Reason. 41(2), 143\u2013189 (2008)","journal-title":"J. Autom. Reason."},{"key":"9497_CR57","doi-asserted-by":"crossref","unstructured":"Platzer, A., Clarke, E.M.: Computing differential invariants of hybrid systems as fixedpoints. In: Gupta and Malik [28], pp. 176\u2013189","DOI":"10.1007\/978-3-540-70545-1_17"},{"key":"9497_CR58","unstructured":"Platzer, A., Quesel, J.: KeYmaera: a hybrid theorem prover for hybrid systems (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12\u201315, 2008, Proceedings, Volume 5195 of LNCS, pp. 171\u2013178. Springer (2008)"},{"key":"9497_CR59","unstructured":"Podelski, A., Wagner, S.: Model checking of hybrid systems: from reachability towards stability. In: Hespanha, J.P., Tiwari, A. (eds.) Hybrid Systems: Computation and Control, 9th International Workshop, HSCC 2006, Santa Barbara, CA, USA, March 29\u201331, 2006, Proceedings, Volume 3927 of LNCS, pp. 507\u2013521. Springer (2006)"},{"key":"9497_CR60","unstructured":"Podelski, A., Wagner, S.: Region stability proofs for hybrid systems. In: Raskin, J., Thiagarajan, P.S. (eds.) Formal Modeling and Analysis of Timed Systems, 5th International Conference, FORMATS 2007, Salzburg, Austria, October 3\u20135, 2007, Proceedings, Volume 4763 of LNCS, pp. 320\u2013335. Springer (2007)"},{"key":"9497_CR61","doi-asserted-by":"crossref","unstructured":"Podelski, A., Wagner, S.: A sound and complete proof rule for region stability of hybrid systems. In: Bemporad et\u00a0al. [4], pp. 750\u2013753","DOI":"10.1007\/978-3-540-71493-4_76"},{"key":"9497_CR62","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-642-39799-8_20","volume-title":"Computer Aided Verification","author":"Pavithra Prabhakar","year":"2013","unstructured":"Prabhakar, P., Soto, M.G.: Abstraction based model-checking of stability of hybrid systems. In: Sharygina and Veith [69], pp. 280\u2013295"},{"key":"9497_CR63","doi-asserted-by":"crossref","unstructured":"Prajna, S., Jadbabaie, A.: Safety verification of hybrid systems using barrier certificates. In: Alur, R., Pappas, G.J. (eds.) Hybrid Systems: Computation and Control, 7th International Workshop, HSCC 2004, Philadelphia, PA, USA, March 25\u201327, 2004, Proceedings, Volume 2993 of LNCS, pp. 477\u2013492. Springer (2004)","DOI":"10.1007\/978-3-540-24743-2_32"},{"issue":"7","key":"9497_CR64","doi-asserted-by":"publisher","first-page":"4377","DOI":"10.1137\/090749955","volume":"48","author":"S Ratschan","year":"2010","unstructured":"Ratschan, S., She, Z.: Providing a basin of attraction to a target region of polynomial systems by computation of Lyapunov-like functions. SIAM J. Control Optim. 48(7), 4377\u20134394 (2010)","journal-title":"SIAM J. Control Optim."},{"key":"9497_CR65","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1016\/j.tcs.2015.06.018","volume":"594","author":"R Rebiha","year":"2015","unstructured":"Rebiha, R., Moura, A.V., Matringe, N.: Generating invariants for non-linear hybrid systems. Theor. Comput. Sci. 594, 180\u2013200 (2015)","journal-title":"Theor. Comput. Sci."},{"key":"9497_CR66","first-page":"12","volume":"33(4), 514\u2013520","author":"D Richardson","year":"1968","unstructured":"Richardson, D.: Some undecidable problems involving elementary functions of a real variable. J. Symb. Logic 33(4), 514\u2013520, 12 (1968)","journal-title":"J. Symb. Logic"},{"key":"9497_CR67","unstructured":"Sankaranarayanan, S.: Automatic invariant generation for hybrid systems using ideal fixed points. In: Johansson, K.H., Yi, W. (eds.) Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2010, Stockholm, Sweden, April 12\u201315, 2010, pp. 221\u2013230. ACM (2010)"},{"issue":"1","key":"9497_CR68","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/s10703-007-0046-1","volume":"32","author":"S Sankaranarayanan","year":"2008","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constructing invariants for hybrid systems. Form. Methods Syst. Des. 32(1), 25\u201355 (2008)","journal-title":"Form. Methods Syst. Des."},{"key":"9497_CR69","doi-asserted-by":"crossref","unstructured":"Sharygina, N., Veith, H. (eds.): Computer Aided Verification\u201425th International Conference, CAV 2013, Saint Petersburg, Russia, July 13\u201319, 2013. Proceedings, Volume 8044 of LNCS. Springer (2013)","DOI":"10.1007\/978-3-642-39799-8"},{"key":"9497_CR70","doi-asserted-by":"crossref","unstructured":"Sogokon, A., Ghorbal, K., Jackson, P.B., Platzer, A.: A method for invariant generation for polynomial continuous systems. In: Jobstmann, B., Leino, K.R.M. (eds.) Verification, Model Checking, and Abstract Interpretation\u201417th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17\u201319, 2016. Proceedings, Volume 9583 of LNCS, pp. 268\u2013288. Springer (2016)","DOI":"10.1007\/978-3-662-49122-5_13"},{"issue":"5","key":"9497_CR71","first-page":"185:1","volume":"16","author":"A Sogokon","year":"2017","unstructured":"Sogokon, A., Ghorbal, K., Johnson, T.T.: Operational models for piecewise-smooth systems. ACM Trans. Embed. Comput. Syst. 16(5), 185:1\u2013185:19 (2017)","journal-title":"ACM Trans. Embed. Comput. Syst."},{"key":"9497_CR72","doi-asserted-by":"crossref","unstructured":"Sogokon, A., Jackson, P.B.: Direct formal verification of liveness properties in continuous and hybrid dynamical systems. In: Bj\u00f8rner, N., de\u00a0Boer, F.S. (eds.) FM 2015: Formal Methods\u201420th International Symposium, Oslo, Norway, June 24\u201326, 2015, Proceedings, Volume 9109 of LNCS, pp. 514\u2013531. Springer (2015)","DOI":"10.1007\/978-3-319-19249-9_32"},{"issue":"11","key":"9497_CR73","doi-asserted-by":"publisher","first-page":"1284","DOI":"10.1016\/j.jsc.2011.08.009","volume":"46","author":"AW Strzebo\u0144ski","year":"2011","unstructured":"Strzebo\u0144ski, A.W.: Cylindrical decomposition for systems transcendental in the first variable. J. Symb. Comput. 46(11), 1284\u20131290 (2011)","journal-title":"J. Symb. Comput."},{"key":"9497_CR74","unstructured":"Taly, A., Tiwari, A.: Deductive verification of continuous dynamical systems. In: Kannan, R., Kumar, K.N. (eds.) IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2009, December 15\u201317, 2009, IIT Kanpur, India, Volume\u00a04 of LIPIcs, pp. 383\u2013394. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2009)"},{"key":"9497_CR75","unstructured":"Tiwari, A.: Generating box invariants. In: Egerstedt, M., Mishra, B. (eds.) Hybrid Systems: Computation and Control, 11th International Workshop, HSCC 2008, St. Louis, MO, USA, April 22\u201324, 2008. Proceedings, Volume 4981 of LNCS, pp. 658\u2013661. Springer (2008)"},{"issue":"1","key":"9497_CR76","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1016\/0005-1098(85)90099-8","volume":"21","author":"A Vannelli","year":"1985","unstructured":"Vannelli, A., Vidyasagar, M.: Maximal Lyapunov functions and domains of attraction for autonomous nonlinear systems. Automatica 21(1), 69\u201380 (1985)","journal-title":"Automatica"},{"key":"9497_CR77","doi-asserted-by":"crossref","unstructured":"Wang, S., Zhan, N., Zou, L.: An improved HHL prover: an interactive theorem prover for hybrid systems. In: Butler, M.J., Conchon, S., Za\u00efdi, F. (eds.) Formal Methods and Software Engineering\u201417th International Conference on Formal Engineering Methods, ICFEM 2015, Paris, France, November 3\u20135, 2015, Proceedings, Volume 9407 of LNCS, pp. 382\u2013399. Springer (2015)","DOI":"10.1007\/978-3-319-25423-4_25"},{"issue":"7","key":"9497_CR78","doi-asserted-by":"publisher","first-page":"3518","DOI":"10.1109\/TAC.2016.2615599","volume":"62","author":"B Xue","year":"2017","unstructured":"Xue, B., Easwaran, A., Cho, N., Fr\u00e4nzle, M.: Reach-avoid verification for nonlinear systems based on boundary analysis. IEEE Trans. Autom. Control 62(7), 3518\u20133523 (2017)","journal-title":"IEEE Trans. Autom. Control"},{"key":"9497_CR79","doi-asserted-by":"crossref","unstructured":"Zhao, H., Yang, M., Zhan, N., Gu, B., Zou, L., Chen, Y.: Formal verification of a descent guidance control program of a lunar lander. In: Jones, C.B., Pihlajasaari, P., Sun, J. (eds.) FM 2014: Formal Methods\u201419th International Symposium, Singapore, May 12\u201316, 2014. Proceedings, Volume 8442 of LNCS, pp. 733\u2013748. Springer (2014)","DOI":"10.1007\/978-3-319-06410-9_49"},{"key":"9497_CR80","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-642-39698-4_22","volume-title":"Theories of Programming and Formal Methods","author":"Hengjun Zhao","year":"2013","unstructured":"Zhao, H., Zhan, N., Kapur, D.: Synthesizing switching controllers for hybrid systems by generating invariants. In: Theories of Programming and Formal Methods\u2014Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday, pp. 354\u2013373 (2013)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-9497-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-018-9497-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-9497-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,4]],"date-time":"2026-04-04T05:38:05Z","timestamp":1775281085000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-018-9497-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,11,24]]},"references-count":80,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2019,12]]}},"alternative-id":["9497"],"URL":"https:\/\/doi.org\/10.1007\/s10817-018-9497-x","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,11,24]]},"assertion":[{"value":"15 November 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 November 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 November 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}