{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T05:36:21Z","timestamp":1743140181620,"version":"3.40.3"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319489889"},{"type":"electronic","value":"9783319489896"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-48989-6_38","type":"book-chapter","created":{"date-parts":[[2016,11,7]],"date-time":"2016-11-07T06:31:19Z","timestamp":1478500279000},"page":"628-644","source":"Crossref","is-referenced-by-count":1,"title":["Decoupling Abstractions of Non-linear Ordinary Differential Equations"],"prefix":"10.1007","author":[{"given":"Andrew","family":"Sogokon","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Khalil","family":"Ghorbal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Taylor T.","family":"Johnson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,11,8]]},"reference":[{"key":"38_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-642-30885-7_13","volume-title":"Abstract State Machines, Alloy, B, VDM, and Z","author":"J-R Abrial","year":"2012","unstructured":"Abrial, J.-R., Su, W., Zhu, H.: Formalizing hybrid systems with Event-B. In: Derrick, J., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) ABZ 2012. LNCS, vol. 7316, pp. 178\u2013193. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-30885-7_13"},{"key":"38_CR2","doi-asserted-by":"crossref","unstructured":"Bak, S., Bogomolov, S., Johnson, T.T.: HYST: a source transformation and translation tool for hybrid automaton models. In: HSCC, pp. 128\u2013133. ACM (2015)","DOI":"10.1145\/2728606.2728630"},{"issue":"4","key":"38_CR3","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. Reliable Comput. 4(4), 361\u2013369 (1998)","journal-title":"Reliable Comput."},{"key":"38_CR4","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":"38_CR5","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-3-540-45204-1_2","volume-title":"Dynamical Systems","author":"R Conti","year":"2003","unstructured":"Conti, R., Galeotti, M.: Totally bounded cubic systems in $$\\mathbb{R}^2$$ R 2 . In: Macki, J.W., Zecca, P. (eds.) Dynamical Systems. LNM, vol. 1822, pp. 103\u2013171. Springer, Heidelberg (2003). doi: 10.1007\/978-3-540-45204-1_2"},{"key":"38_CR6","volume-title":"Qualitative Theory of Planar Differential Systems","author":"F Dumortier","year":"2006","unstructured":"Dumortier, F., Llibre, J., Art\u00e9s, J.C.: Qualitative Theory of Planar Differential Systems. Springer, Heidelberg (2006)"},{"key":"38_CR7","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":"38_CR8","series-title":"Lecture Notes in Computer Science","volume-title":"FM 2012: Formal Methods","year":"2012","unstructured":"Giannakopoulou, D., M\u00e9ry, D. (eds.): FM 2012. LNCS, vol. 7436. Springer, Heidelberg (2012)"},{"key":"38_CR9","series-title":"World Scientific Series on Nonlinear Science","doi-asserted-by":"crossref","DOI":"10.1142\/7333","volume-title":"Differential Geometry Applied to Dynamical Systems","author":"JM Ginoux","year":"2009","unstructured":"Ginoux, J.M.: Differential Geometry Applied to Dynamical Systems. World Scientific Series on Nonlinear Science, vol. 66. World Scientific, Singapore (2009)"},{"issue":"5\u20136","key":"38_CR10","doi-asserted-by":"crossref","first-page":"568","DOI":"10.3166\/ejc.17.568-578","volume":"17","author":"A Girard","year":"2011","unstructured":"Girard, A., Pappas, G.J.: Approximate bisimulation: a bridge between computer science and control theory. Eur. J. Control 17(5\u20136), 568\u2013578 (2011)","journal-title":"Eur. J. Control"},{"key":"38_CR11","series-title":"Advanced Series in Nonlinear Dynamics","doi-asserted-by":"crossref","DOI":"10.1142\/3846","volume-title":"Integrability and Nonintegrability of Dynamical Systems","author":"A Goriely","year":"2001","unstructured":"Goriely, A.: Integrability and Nonintegrability of Dynamical Systems. Advanced Series in Nonlinear Dynamics. World Scientific, Singapore (2001)"},{"issue":"3","key":"38_CR12","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1137\/1005068","volume":"5","author":"JK Hale","year":"1963","unstructured":"Hale, J.K., LaSalle, J.P.: Differential equations: linearity vs. nonlinearity. SIAM Rev. 5(3), 249\u2013272 (1963)","journal-title":"SIAM Rev."},{"key":"38_CR13","unstructured":"Han, Z., Krogh, B.: Reachability analysis of hybrid control systems using reduced-order models. In: 2004 American Control Conference, Proceedings of the 2004, vol. 2, pp. 1183\u20131189, June 2004"},{"key":"38_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-662-46681-0_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J-B Jeannin","year":"2015","unstructured":"Jeannin, J.-B., Ghorbal, K., Kouskoulas, Y., Gardner, R., Schmidt, A., Zawadzki, E., Platzer, A.: A formally verified hybrid system for the next-generation airborne collision avoidance system. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 21\u201336. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-46681-0_2"},{"key":"38_CR15","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":"38_CR16","unstructured":"Nedialkov, N.S.: Interval tools for ODEs and DAEs. In: 12th GAMM - IMACS International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics (SCAN), p. 4, September 2006"},{"issue":"1","key":"38_CR17","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."},{"issue":"12","key":"38_CR18","doi-asserted-by":"crossref","first-page":"2035","DOI":"10.1016\/j.automatica.2003.07.003","volume":"39","author":"GJ Pappas","year":"2003","unstructured":"Pappas, G.J.: Bisimilar linear systems. Automatica 39(12), 2035\u20132047 (2003)","journal-title":"Automatica"},{"key":"38_CR19","doi-asserted-by":"crossref","unstructured":"Platzer, A.: A complete uniform substitution calculus for differential dynamic logic. J. Autom. Reasoning, 1\u201347 (2016)","DOI":"10.1007\/s10817-016-9385-1"},{"key":"38_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"547","DOI":"10.1007\/978-3-642-05089-3_35","volume-title":"FM 2009: Formal Methods","author":"A Platzer","year":"2009","unstructured":"Platzer, A., Clarke, E.M.: Formal verification of curved flight collision avoidance maneuvers: a case study. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 547\u2013562. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-05089-3_35"},{"key":"38_CR21","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511801204","volume-title":"An Introduction to Ordinary Differential Equations","author":"JC Robinson","year":"2004","unstructured":"Robinson, J.C.: An Introduction to Ordinary Differential Equations. Cambridge University Press, Cambridge (2004)"},{"key":"38_CR22","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1016\/j.nahs.2015.08.006","volume":"19","author":"S Sankaranarayanan","year":"2016","unstructured":"Sankaranarayanan, S.: Change-of-bases abstractions for non-linear hybrid systems. Nonlinear Anal. Hybrid Syst. 19, 107\u2013133 (2016)","journal-title":"Nonlinear Anal. Hybrid Syst."},{"issue":"1","key":"38_CR23","doi-asserted-by":"crossref","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. Formal Methods Syst. Des. 32(1), 25\u201355 (2008)","journal-title":"Formal Methods Syst. Des."},{"key":"38_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"686","DOI":"10.1007\/978-3-642-22110-1_56","volume-title":"Computer Aided Verification","author":"S Sankaranarayanan","year":"2011","unstructured":"Sankaranarayanan, S., Tiwari, A.: Relational abstractions for continuous and hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 686\u2013702. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-22110-1_56"},{"key":"38_CR25","volume-title":"Nonlinear Dynamics and Chaos","author":"SH Strogatz","year":"1994","unstructured":"Strogatz, S.H.: Nonlinear Dynamics and Chaos. Westview Press, New York (1994)"},{"key":"38_CR26","doi-asserted-by":"crossref","unstructured":"Tarski, A.: A decision method for elementary algebra and geometry. In: Bulletin of the American Mathematical Society, vol. 59 (1951)","DOI":"10.1525\/9780520348097"},{"key":"38_CR27","series-title":"Graduate Studies in Mathematics","doi-asserted-by":"crossref","DOI":"10.1090\/gsm\/140","volume-title":"Ordinary Differential Equations and Dynamical Systems","author":"G Teschl","year":"2012","unstructured":"Teschl, G.: Ordinary Differential Equations and Dynamical Systems. Graduate Studies in Mathematics, vol. 140. American Mathematical Society, Providence (2012)"},{"key":"38_CR28","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, Heidelberg (2014). doi: 10.1007\/978-3-319-06410-9_49"},{"key":"38_CR29","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). doi: 10.1007\/978-3-642-54108-7_14"}],"container-title":["Lecture Notes in Computer Science","FM 2016: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-48989-6_38","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,12]],"date-time":"2022-07-12T16:29:31Z","timestamp":1657643371000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-48989-6_38"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319489889","9783319489896"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-48989-6_38","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}