{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,19]],"date-time":"2026-02-19T07:14:51Z","timestamp":1771485291321,"version":"3.50.1"},"publisher-location":"Cham","reference-count":63,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319572871","type":"print"},{"value":"9783319572888","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-57288-8_14","type":"book-chapter","created":{"date-parts":[[2017,4,8]],"date-time":"2017-04-08T02:45:05Z","timestamp":1491619505000},"page":"194-211","source":"Crossref","is-referenced-by-count":3,"title":["Verifying Safety and Persistence Properties of Hybrid Systems Using Flowpipes and Continuous Invariants"],"prefix":"10.1007","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":[[2017,4,9]]},"reference":[{"key":"14_CR1","unstructured":"CAPD library. http:\/\/capd.ii.uj.edu.pl\/"},{"issue":"3","key":"14_CR2","doi-asserted-by":"crossref","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":"14_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/3-540-57318-6_30","volume-title":"Hybrid Systems","author":"R Alur","year":"1993","unstructured":"Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.-H.: 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.) HS 1991\u20131992. LNCS, vol. 736, pp. 209\u2013229. Springer, Heidelberg (1993). doi: 10.1007\/3-540-57318-6_30"},{"issue":"4","key":"14_CR4","doi-asserted-by":"crossref","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":"14_CR5","doi-asserted-by":"crossref","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":"14_CR6","unstructured":"Carter, R.A.: Verification of liveness properties on hybrid dynamical systems. Ph.D. thesis, University of Manchester, School of Computer Science (2013)"},{"key":"14_CR7","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). doi: 10.1007\/978-3-642-39799-8_18"},{"issue":"4","key":"14_CR8","doi-asserted-by":"crossref","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."},{"key":"14_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/3-540-07407-4_17","volume-title":"Automata Theory and Formal Languages 2nd GI Conference Kaiserslautern, May 20\u201323, 1975","author":"GE Collins","year":"1975","unstructured":"Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol. 33, pp. 134\u2013183. Springer, Heidelberg (1975). doi: 10.1007\/3-540-07407-4_17"},{"key":"14_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-540-71493-4_16","volume-title":"Hybrid Systems: Computation and Control","author":"A Donz\u00e9","year":"2007","unstructured":"Donz\u00e9, A., Maler, O.: Systematic simulation using sensitivity analysis. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol. 4416, pp. 174\u2013189. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-71493-4_16"},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"Duggirala, P.S., Mitra, S.: Abstraction refinement for stability. In: Proceedings of 2011 IEEE\/ACM International Conference on Cyber-Physical Systems, ICCPS, pp. 22\u201331, April 2011","DOI":"10.1109\/ICCPS.2011.24"},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"Duggirala, P.S., Mitra, S.: Lyapunov abstractions for inevitability of hybrid systems. In: HSCC, pp. 115\u2013124. ACM, New York (2012)","DOI":"10.1145\/2185632.2185652"},{"issue":"1","key":"14_CR13","doi-asserted-by":"crossref","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":"14_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/978-3-642-22110-1_30","volume-title":"Computer Aided Verification","author":"G Frehse","year":"2011","unstructured":"Frehse, G., Guernic, C., 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.) CAV 2011. LNCS, vol. 6806, pp. 379\u2013395. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-22110-1_30"},{"key":"14_CR15","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1007\/978-3-319-21401-6_36","volume-title":"Automated Deduction - CADE-25","author":"N Fulton","year":"2015","unstructured":"Fulton, N., Mitsch, S., Quesel, J.-D., V\u00f6lp, M., Platzer, A.: KeYmaera\u00a0X: an axiomatic tactical theorem prover for hybrid systems. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 527\u2013538. Springer, Cham (2015). doi: 10.1007\/978-3-319-21401-6_36"},{"key":"14_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-642-54862-8_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K Ghorbal","year":"2014","unstructured":"Ghorbal, K., Platzer, A.: Characterizing algebraic invariants by differential radical invariants. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 279\u2013294. Springer, Heidelberg (2014). doi: 10.1007\/978-3-642-54862-8_19"},{"key":"14_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1007\/978-3-662-46081-8_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"K Ghorbal","year":"2015","unstructured":"Ghorbal, K., Sogokon, A., Platzer, A.: A hierarchy of proof rules for checking differential invariance of algebraic sets. In: D\u2019Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 431\u2013448. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-46081-8_24"},{"key":"14_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/978-3-540-70545-1_18","volume-title":"Computer Aided Verification","author":"S Gulwani","year":"2008","unstructured":"Gulwani, S., Tiwari, A.: Constraint-based approach for analysis of hybrid systems. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 190\u2013203. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-70545-1_18"},{"key":"14_CR19","first-page":"278","volume-title":"The Theory of Hybrid Automata","author":"TA Henzinger","year":"1996","unstructured":"Henzinger, T.A.: The Theory of Hybrid Automata, pp. 278\u2013292. IEEE Computer Society Press, Washington, DC (1996)"},{"key":"14_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/978-3-662-46681-0_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F Immler","year":"2015","unstructured":"Immler, F.: Verified reachability analysis of continuous systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 37\u201351. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-46681-0_3"},{"key":"14_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-662-46681-0_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Kong","year":"2015","unstructured":"Kong, S., Gao, S., Chen, W., Clarke, E.: dReach: $$\\delta $$ -reachability analysis for hybrid systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 200\u2013205. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-46681-0_15"},{"issue":"4","key":"14_CR22","doi-asserted-by":"crossref","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":"14_CR23","doi-asserted-by":"crossref","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":"14_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-17164-2_1","volume-title":"Programming Languages and Systems","author":"J Liu","year":"2010","unstructured":"Liu, J., Lv, J., Quan, Z., Zhan, N., Zhao, H., Zhou, C., Zou, L.: A calculus for hybrid CSP. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol. 6461, pp. 1\u201315. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-17164-2_1"},{"key":"14_CR25","doi-asserted-by":"crossref","unstructured":"Liu, J., Zhan, N., Zhao, H.: Computing semi-algebraic invariants for polynomial dynamical systems. In: EMSOFT, pp. 97\u2013106. ACM (2011)","DOI":"10.1145\/2038642.2038659"},{"issue":"1","key":"14_CR26","doi-asserted-by":"crossref","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"},{"issue":"1","key":"14_CR27","doi-asserted-by":"crossref","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"},{"key":"14_CR28","doi-asserted-by":"crossref","unstructured":"Maidens, J.N., Arcak, M.: Trajectory-based reachability analysis of switched nonlinear systems using matrix measures. In: CDC, pp. 6358\u20136364, December 2014","DOI":"10.1109\/CDC.2014.7040386"},{"issue":"1","key":"14_CR29","doi-asserted-by":"crossref","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":"14_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1007\/978-3-642-15769-1_23","volume-title":"Static Analysis","author":"N Matringe","year":"2010","unstructured":"Matringe, N., Moura, A.V., Rebiha, R.: Generating invariants for non-linear hybrid systems by linear algebraic methods. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 373\u2013389. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-15769-1_23"},{"key":"14_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1007\/978-3-642-24310-3_20","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"C Mitrohin","year":"2011","unstructured":"Mitrohin, C., Podelski, A.: Composing stability proofs for hybrid systems. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 286\u2013300. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-24310-3_20"},{"key":"14_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/978-3-319-22975-1_15","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"E M\u00f6hlmann","year":"2015","unstructured":"M\u00f6hlmann, E., Hagemann, W., Theel, O.: Hybrid tools for hybrid systems \u2013 proving stability and safety at once. In: Sankaranarayanan, S., Vicario, E. (eds.) FORMATS 2015. LNCS, vol. 9268, pp. 222\u2013239. Springer, Cham (2015). doi: 10.1007\/978-3-319-22975-1_15"},{"key":"14_CR33","doi-asserted-by":"crossref","unstructured":"M\u00f6hlmann, E., Theel, O.: Stabhyli: a tool for automatic stability verification of non-linear hybrid systems. In: HSCC, pp. 107\u2013112. ACM (2013)","DOI":"10.1145\/2461328.2461347"},{"issue":"11","key":"14_CR34","doi-asserted-by":"crossref","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":"14_CR35","doi-asserted-by":"crossref","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":"14_CR36","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. In: Proceedings of the 2004 IEEE International Conference on Control Applications, vol. 2, pp. 1454\u20131460. IEEE (2004)","DOI":"10.1109\/CCA.2004.1387580"},{"key":"14_CR37","unstructured":"Nedialkov, N.S.: Interval tools for ODEs and DAEs. In: SCAN (2006)"},{"issue":"1","key":"14_CR38","doi-asserted-by":"crossref","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":"14_CR39","unstructured":"Nishida, T., Mizutani, K., Kubota, A., Doshita, S.: Automated phase portrait analysis by integrating qualitative and quantitative analysis. In: Proceedings of the 9th National Conference on Artificial Intelligence, pp. 811\u2013816 (1991)"},{"key":"14_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-32347-8_1","volume-title":"Interactive Theorem Proving","author":"LC Paulson","year":"2012","unstructured":"Paulson, L.C.: MetiTarski: past and future. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 1\u201310. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-32347-8_1"},{"issue":"2","key":"14_CR41","doi-asserted-by":"crossref","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."},{"issue":"1","key":"14_CR42","doi-asserted-by":"crossref","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":"14_CR43","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). doi: 10.1007\/978-3-540-70545-1_17"},{"key":"14_CR44","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-540-71070-7_15","volume-title":"Automated Reasoning","author":"A Platzer","year":"2008","unstructured":"Platzer, A., Quesel, J.-D.: KeYmaera: a hybrid theorem prover for hybrid systems (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 171\u2013178. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-71070-7_15"},{"key":"14_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1007\/11730637_38","volume-title":"Hybrid Systems: Computation and Control","author":"A Podelski","year":"2006","unstructured":"Podelski, A., Wagner, S.: Model checking of hybrid systems: from reachability towards stability. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol. 3927, pp. 507\u2013521. Springer, Heidelberg (2006). doi: 10.1007\/11730637_38"},{"key":"14_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1007\/978-3-540-75454-1_23","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"A Podelski","year":"2007","unstructured":"Podelski, A., Wagner, S.: Region stability proofs for hybrid systems. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 320\u2013335. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-75454-1_23"},{"key":"14_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"750","DOI":"10.1007\/978-3-540-71493-4_76","volume-title":"Hybrid Systems: Computation and Control","author":"A Podelski","year":"2007","unstructured":"Podelski, A., Wagner, S.: A sound and complete proof rule for region stability of hybrid systems. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol. 4416, pp. 750\u2013753. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-71493-4_76"},{"key":"14_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-642-39799-8_20","volume-title":"Computer Aided Verification","author":"P Prabhakar","year":"2013","unstructured":"Prabhakar, P., Garcia Soto, M.: Abstraction based model-checking of stability of hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 280\u2013295. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39799-8_20"},{"key":"14_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/978-3-540-24743-2_32","volume-title":"Hybrid Systems: Computation and Control","author":"S Prajna","year":"2004","unstructured":"Prajna, S., Jadbabaie, A.: Safety verification of hybrid systems using barrier certificates. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 477\u2013492. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-24743-2_32"},{"issue":"7","key":"14_CR50","doi-asserted-by":"crossref","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."},{"issue":"4","key":"14_CR51","doi-asserted-by":"crossref","first-page":"514","DOI":"10.2307\/2271358","volume":"33","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 (1968)","journal-title":"J. Symb. Logic"},{"key":"14_CR52","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S.: Automatic invariant generation for hybrid systems using ideal fixed points. In: HSCC, pp. 221\u2013230 (2010)","DOI":"10.1145\/1755952.1755984"},{"issue":"1","key":"14_CR53","first-page":"25","volume":"32","author":"S Sankaranarayanan","year":"2008","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constructing invariants for hybrid systems. FMSD 32(1), 25\u201355 (2008)","journal-title":"FMSD"},{"key":"14_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/978-3-662-49122-5_13","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Sogokon","year":"2016","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.) VMCAI 2016. LNCS, vol. 9583, pp. 268\u2013288. Springer, Heidelberg (2016). doi: 10.1007\/978-3-662-49122-5_13"},{"key":"14_CR55","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"514","DOI":"10.1007\/978-3-319-19249-9_32","volume-title":"FM 2015: Formal Methods","author":"A Sogokon","year":"2015","unstructured":"Sogokon, A., Jackson, P.B.: Direct formal verification of liveness properties in continuous and hybrid dynamical systems. In: Bj\u00f8rner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 514\u2013531. Springer, Cham (2015). doi: 10.1007\/978-3-319-19249-9_32"},{"key":"14_CR56","doi-asserted-by":"crossref","unstructured":"Sogokon, A., Jackson, P.B., Johnson, T.T.: Verifying safety and persistence properties of hybrid systems using flowpipes and continuous invariants. Technical report, Vanderbilt University (2017)","DOI":"10.1007\/s10817-018-9497-x"},{"issue":"11","key":"14_CR57","doi-asserted-by":"crossref","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":"14_CR58","unstructured":"Taly, A., Tiwari, A.: Deductive verification of continuous dynamical systems. In: Kannan, R., Kumar, K.N. (eds.) FSTTCS. LIPIcs, vol. 4, pp. 383\u2013394. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Wadern (2009)"},{"key":"14_CR59","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"658","DOI":"10.1007\/978-3-540-78929-1_58","volume-title":"Hybrid Systems: Computation and Control","author":"A Tiwari","year":"2008","unstructured":"Tiwari, A.: Generating box invariants. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 658\u2013661. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-78929-1_58"},{"key":"14_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/978-3-319-25423-4_25","volume-title":"Formal Methods and Software Engineering","author":"S Wang","year":"2015","unstructured":"Wang, S., Zhan, N., Zou, L.: An improved HHL prover: an interactive theorem prover for hybrid systems. In: Butler, M., Conchon, S., Za\u00efdi, F. (eds.) ICFEM 2015. LNCS, vol. 9407, pp. 382\u2013399. Springer, Cham (2015). doi: 10.1007\/978-3-319-25423-4_25"},{"key":"14_CR61","doi-asserted-by":"crossref","unstructured":"Xue, B., Easwaran, A., Cho, N.J., Fr\u00e4nzle, M.: Reach-avoid verification for nonlinear systems based on boundary analysis. IEEE Trans. Autom. Control (2016)","DOI":"10.1109\/TAC.2016.2615599"},{"key":"14_CR62","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1007\/978-3-319-06410-9_49","volume-title":"FM 2014: Formal Methods","author":"H Zhao","year":"2014","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., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 733\u2013748. Springer, Cham (2014). doi: 10.1007\/978-3-319-06410-9_49"},{"key":"14_CR63","series-title":"Lecture Notes in Computer Science","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":"H Zhao","year":"2013","unstructured":"Zhao, H., Zhan, N., Kapur, D.: Synthesizing switching controllers for hybrid systems by generating invariants. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) Theories of Programming and Formal Methods. LNCS, vol. 8051, pp. 354\u2013373. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39698-4_22"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-57288-8_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,20]],"date-time":"2019-09-20T16:28:39Z","timestamp":1568996919000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-57288-8_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319572871","9783319572888"],"references-count":63,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-57288-8_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}