{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,21]],"date-time":"2026-02-21T18:13:35Z","timestamp":1771697615117,"version":"3.50.1"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319415277","type":"print"},{"value":"9783319415284","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"vor","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":[[2016]]},"DOI":"10.1007\/978-3-319-41528-4_25","type":"book-chapter","created":{"date-parts":[[2016,7,12]],"date-time":"2016-07-12T09:34:06Z","timestamp":1468316046000},"page":"457-476","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":32,"title":["Under-Approximating Backward Reachable Sets by Polytopes"],"prefix":"10.1007","author":[{"given":"Bai","family":"Xue","sequence":"first","affiliation":[]},{"given":"Zhikun","family":"She","sequence":"additional","affiliation":[]},{"given":"Arvind","family":"Easwaran","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,7,13]]},"reference":[{"key":"25_CR1","unstructured":"Xue, B.: Computing rigor quadratic lyapunov functions and underapproximate reachable sets for ordinary differential equations. Doctoral dissertation, Beihang University (2013)"},{"key":"25_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1210268.1210276","volume":"6","author":"S Ratschan","year":"2007","unstructured":"Ratschan, S., She, Z.: Safety verification of hybrid systems by constraint propagation-based abstraction refinement. ACM Trans. Embed. Comput. Syst. 6, 1\u201323 (2007)","journal-title":"ACM Trans. Embed. Comput. Syst."},{"key":"25_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1007\/978-3-540-73368-3_48","volume-title":"Computer Aided Verification","author":"E Plaku","year":"2007","unstructured":"Plaku, E., Kavraki, L.E., Vardi, M.Y.: Hybrid systems: from verification to falsification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 463\u2013476. Springer, Heidelberg (2007)"},{"key":"25_CR4","doi-asserted-by":"publisher","first-page":"1131","DOI":"10.1177\/193229681200600518","volume":"6","author":"P Herrero","year":"2012","unstructured":"Herrero, P., Calm, R., Veh\u00ed, J., Armengol, J., Georgiou, P., Oliver, N., Tomazou, C.: Robust fault detection system for insulin pump therapy using continuous glucose monitoring. J. Diabetes Sci. Technol. 6, 1131\u20131141 (2012)","journal-title":"J. Diabetes Sci. Technol."},{"key":"25_CR5","unstructured":"Xue, B., Easwaran, A., Cho, N.: Towards robust artificial pancreas based on reachability analysis techniques. In: Workshop on Medical Cyber-Physical Systems (2015)"},{"key":"25_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1109\/TRO.2014.2312453","volume":"30","author":"M Althoff","year":"2014","unstructured":"Althoff, M., Dolan, J.M.: Online verification of automated road vehicles using reachability analysis. IEEE Trans. Robot. 30, 1\u201316 (2014)","journal-title":"IEEE Trans. Robot."},{"key":"25_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/3-540-36580-X_4","volume-title":"Hybrid Systems: Computation and Control","author":"R Alur","year":"2003","unstructured":"Alur, R., Dang, T., Ivan\u010di\u0107, F.: Progress on reachability analysis of hybrid systems using predicate abstraction. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 4\u201319. Springer, Heidelberg (2003)"},{"issue":"7","key":"25_CR8","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1007\/s00236-006-0035-7","volume":"43","author":"E Asarin","year":"2007","unstructured":"Asarin, E., Dang, T., Girard, A.: Hybridization methods for the analysis of nonlinear systems. Acta Inf. 43(7), 451\u2013476 (2007)","journal-title":"Acta Inf."},{"key":"25_CR9","doi-asserted-by":"crossref","unstructured":"Huang, Z., Mitra, S.: Proofs from simulations and modular annotations. In: Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control (HSCC 2014), pp. 183\u2013192. ACM, New York (2014)","DOI":"10.1145\/2562059.2562126"},{"key":"25_CR10","doi-asserted-by":"crossref","unstructured":"Chen, X., \u00c1brah\u00e1m, E., Sankaranarayanan, S.: Taylor model flowpipe construction for non-linear hybrid systems. In: Proceedings of the 2012 IEEE 33rd Real-Time Systems Symposium (RTSS 2012), pp. 183\u2013192. IEEE Computer Society, Washington (2012)","DOI":"10.1109\/RTSS.2012.70"},{"key":"25_CR11","doi-asserted-by":"crossref","unstructured":"Althoff, M.: Reachability analysis of nonlinear systems using conservative polynomialization and non-convex sets. In: Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control (HSCC 2013), pp. 173\u2013182. ACM, New York (2013)","DOI":"10.1145\/2461328.2461358"},{"key":"25_CR12","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1109\/TBME.2010.2058805","volume":"58","author":"A Revert","year":"2011","unstructured":"Revert, A., Calm, R., Vehi, J., Bondia, J.: Calculation of the best basal-bolus combination for postprandial glucose control in insulin pump therapy. IEEE Trans Biomed. Eng. 58, 274\u2013281 (2011)","journal-title":"IEEE Trans Biomed. Eng."},{"issue":"7","key":"25_CR13","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":"25_CR14","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1016\/S0167-6911(00)00059-1","volume":"41","author":"AB Kurzhanski","year":"2000","unstructured":"Kurzhanski, A.B., Varaiya, P.: Ellipsoidal techniques for reachability analysis: internal approximation. Syst. Control Lett. 41, 201\u2013211 (2000)","journal-title":"Syst. Control Lett."},{"key":"25_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/11730637_21","volume-title":"Hybrid Systems: Computation and Control","author":"A Girard","year":"2006","unstructured":"Girard, A., Le Guernic, C., Maler, O.: Efficient computation of reachable sets of linear time-invariant systems with inputs. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol. 3927, pp. 257\u2013271. Springer, Heidelberg (2006)"},{"key":"25_CR16","doi-asserted-by":"publisher","first-page":"2017","DOI":"10.1016\/j.automatica.2013.03.020","volume":"49","author":"JN Maidensa","year":"2013","unstructured":"Maidensa, J.N., Kaynamaa, S., Mitchell, I.M., Oishic, M.K., Dumonta, G.A.: Lagrangian methods for approximating the viability kernel in high-dimensional systems. Automatica 49, 2017\u20132029 (2013)","journal-title":"Automatica"},{"issue":"2","key":"25_CR17","doi-asserted-by":"crossref","first-page":"8960","DOI":"10.3182\/20080706-5-KR-1001.01513","volume":"41","author":"Luca Benvenuti","year":"2008","unstructured":"Benvenuti, L., Bresolin, D., Casagrande, A., Collins, P., Ferrari, A., Mazzi, E., Sangiovanni-Vincentelli, A., Villa, T.: Reachability computation for hybrid systems with Ariadne. In: Proceedings of the 17th IFAC World Congress, vol. 41, pp. 8960\u20138965. IFAC Papers-OnLine (2008)","journal-title":"IFAC Proceedings Volumes"},{"key":"25_CR18","first-page":"1","volume":"14","author":"A Goldsztejn","year":"2010","unstructured":"Goldsztejn, A., Jaulin, L.: Inner approximation of the range of vector-valued functions. Reliable Comput. 14, 1\u201323 (2010)","journal-title":"Reliable Comput."},{"key":"25_CR19","first-page":"117","volume":"18","author":"O Mullier","year":"2013","unstructured":"Mullier, O., Goubault, E., Kieffer, M., Putot, S.: General inner approximation of vector-valued functions. Reliable Comput. 18, 117\u2013143 (2013)","journal-title":"Reliable Comput."},{"key":"25_CR20","doi-asserted-by":"crossref","unstructured":"Goubault, E., Mullier, O., Putot, S., Kieffer, M.: Inner approximated reachability analysis. In: Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control (HSCC 2014), pp. 163\u2013172. ACM, New York (2014)","DOI":"10.1145\/2562059.2562113"},{"key":"25_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/978-3-540-71493-4_34","volume-title":"Hybrid Systems: Computation and Control","author":"IM Mitchell","year":"2007","unstructured":"Mitchell, I.M.: Comparing forward and backward reachability as tools for safety analysis. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol. 4416, pp. 428\u2013443. Springer, Heidelberg (2007)"},{"issue":"23","key":"25_CR22","doi-asserted-by":"crossref","first-page":"534","DOI":"10.3182\/20130904-3-FR-2041.00002","volume":"46","author":"Milan Korda","year":"2013","unstructured":"Korda, M., Henrion, D., Jones, N.C.: Inner approximations of the region of attraction for polynomial dynamical systems. In: Proceedings of 9th IFAC Symposium on Nonlinear Control Systems, pp. 534\u2013539 (2013)","journal-title":"IFAC Proceedings Volumes"},{"key":"25_CR23","doi-asserted-by":"crossref","unstructured":"Chen, X., Sankaranarayanan, S., \u00c1brah\u00e1m, E.: Under-approximate flowpipes fornon-linear continuous systems. In: Proceedings of the 14th Conference on Formal Methods in Computer-Aided Design (FMCAD 2014), pp. 59\u201366. IEEE (2014)","DOI":"10.1109\/FMCAD.2014.6987596"},{"key":"25_CR24","unstructured":"Nedialkov, N.S.: VNODE-LP - a validated solver for initial value problems in ordinary differential equations. Technical report CAS-06-06-NN, Department of Computing and Software, McMaster University, Hamilton, Canada, L8S4K1 (2006). VNODE-LP is available at www.cas.mcmaster.ca\/nedialk\/vnodelp\/"},{"key":"25_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"482","DOI":"10.1007\/3-540-36580-X_35","volume-title":"Hybrid Systems: Computation and Control","author":"O Stursberg","year":"2003","unstructured":"Stursberg, O., Krogh, B.H.: Efficient representation and computation of reachable sets for hybrid systems. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 482\u2013497. Springer, Heidelberg (2003)"},{"key":"25_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1007\/978-3-319-02444-8_37","volume-title":"Automated Technology for Verification and Analysis","author":"R Testylier","year":"2013","unstructured":"Testylier, R., Dang, T.: NLTOOLBOX: a library for reachability computation of nonlinear dynamical systems. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 469\u2013473. Springer, Heidelberg (2013)"},{"key":"25_CR27","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, 121\u2013148 (2015)","journal-title":"Softw. Syst. Model."},{"key":"25_CR28","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4939-9063-4","volume-title":"A Basic Course in Algebraic Topology","author":"WS Massey","year":"1991","unstructured":"Massey, W.S.: A Basic Course in Algebraic Topology. Springer, New York (1991). Corollary 6.7"},{"key":"25_CR29","first-page":"188","volume-title":"Nonlinear Systems","author":"HK Khalil","year":"2002","unstructured":"Khalil, H.K.: Nonlinear Systems, 3rd edn, p. 188. Prentice Hall, Upper Saddle River (2002)","edition":"3"},{"issue":"1","key":"25_CR30","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1145\/1132973.1132980","volume":"32","author":"L Granvilliers","year":"2006","unstructured":"Granvilliers, L., Benhamou, F.: Realpaver: an interval solver using constraint satisfaction techniques. ACM TOMS 32(1), 138\u2013156 (2006)","journal-title":"ACM TOMS"},{"key":"25_CR31","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1109\/JPROC.2011.2165329","volume":"100","author":"Y Susuki","year":"2012","unstructured":"Susuki, Y., Koo, T.J., Ebina, H., Yamazaki, T., Ochi, T., Uemura, T., Hikihara, T.: A hybrid system approach to the analysis and design of power grid dynamic performance. Proc. IEEE 100, 225\u2013239 (2012)","journal-title":"Proc. IEEE"},{"key":"25_CR32","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/j.nahs.2010.05.010","volume":"5","author":"N Ramdani","year":"2011","unstructured":"Ramdani, N., Nedialkov, N.S.: Computing reachable sets for uncertain nonlinear hybrid systems using interval constraint-propagation techniques. Nonlinear Anal. Hybrid Syst. 5, 149\u2013162 (2011)","journal-title":"Nonlinear Anal. Hybrid Syst."},{"key":"25_CR33","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1145\/235815.235821","volume":"22","author":"CB Barber","year":"1996","unstructured":"Barber, C.B., Dobkin, D.P., Huhdanpaa, H.: The quickhull algorithm for convex hulls. ACM Trans. Math. Softw. 22, 469\u2013483 (1996)","journal-title":"ACM Trans. Math. Softw."},{"key":"25_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"407","DOI":"10.1007\/978-3-319-08867-9_27","volume-title":"Computer Aided Verification","author":"W Hagemann","year":"2014","unstructured":"Hagemann, W.: Reachability analysis of hybrid systems using symbolic orthogonal projections. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 407\u2013423. Springer, Heidelberg (2014)"},{"key":"25_CR35","doi-asserted-by":"crossref","unstructured":"L\u00f6fberg, J.: YALMIP: a toolbox for modeling and optimization in MATLAB. In: Proceedings of the CACSD Conference, Taipei, Taiwan, pp. 284\u2013289 (2004)","DOI":"10.1109\/CACSD.2004.1393890"},{"key":"25_CR36","doi-asserted-by":"publisher","first-page":"625","DOI":"10.1080\/10556789908805766","volume":"11","author":"JF Sturm","year":"1999","unstructured":"Sturm, J.F.: Using SeDuMi 1.02, a MATLAB toolbox for optimization over symmetric cones. Optim. Methods Softw. 11, 625\u2013653 (1999)","journal-title":"Optim. Methods Softw."},{"issue":"10","key":"25_CR37","doi-asserted-by":"publisher","first-page":"2508","DOI":"10.1109\/TAC.2013.2263916","volume":"58","author":"T Wang","year":"2013","unstructured":"Wang, T., Lall, S., West, M.: Polynomial level-set method for polynomial system reachable set estimation. IEEE Trans. Autom. Control 58(10), 2508\u20132521 (2013)","journal-title":"IEEE Trans. Autom. Control"},{"key":"25_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/978-3-319-21668-3_20","volume-title":"Computer Aided Verification","author":"L Zou","year":"2015","unstructured":"Zou, L., Fr\u00e4nzle, M., Zhan, N., Mosaad, P.N.: Automatic verification of stability and safety for delay differential equations. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 338\u2013355. Springer, Heidelberg (2015)"},{"key":"25_CR39","doi-asserted-by":"crossref","unstructured":"Majumdar, R., Prabhu, V.S.: Computing distances between reach flowpipes. In: Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control (HSCC 2016), pp. 267\u2013276. ACM, New York (2016)","DOI":"10.1145\/2883817.2883850"}],"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-41528-4_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,4]],"date-time":"2025-06-04T00:41:38Z","timestamp":1748997698000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-41528-4_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319415277","9783319415284"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-41528-4_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"13 July 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Toronto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2016","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 July 2016","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 July 2016","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2016","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}