{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T14:56:58Z","timestamp":1784905018252,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642221095","type":"print"},{"value":"9783642221101","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-22110-1_30","type":"book-chapter","created":{"date-parts":[[2011,7,4]],"date-time":"2011-07-04T09:08:45Z","timestamp":1309770525000},"page":"379-395","source":"Crossref","is-referenced-by-count":506,"title":["SpaceEx: Scalable Verification of Hybrid Systems"],"prefix":"10.1007","author":[{"given":"Goran","family":"Frehse","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Colas","family":"Le Guernic","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alexandre","family":"Donz\u00e9","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Scott","family":"Cotton","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rajarshi","family":"Ray","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Olivier","family":"Lebeltel","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rodolfo","family":"Ripado","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Antoine","family":"Girard","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thao","family":"Dang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Oded","family":"Maler","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"issue":"1","key":"30_CR1","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","volume":"138","author":"R. Alur","year":"1995","unstructured":"Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.-H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theoretical Computer Science\u00a0138(1), 3\u201334 (1995)","journal-title":"Theoretical Computer Science"},{"issue":"7","key":"30_CR2","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.\u00a043(7), 451\u2013476 (2007)","journal-title":"Acta Inf."},{"key":"30_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/3-540-46430-1_6","volume-title":"Hybrid Systems: Computation and Control","author":"E. Asarin","year":"2000","unstructured":"Asarin, E., Bournez, O., Dang, T., Maler, O.: Approximate reachability analysis of piecewise-linear dynamical systems. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol.\u00a01790, p. 20. Springer, Heidelberg (2000)"},{"key":"30_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/978-3-642-15643-4_5","volume-title":"Automated Technology for Verification and Analysis","author":"E. Asarin","year":"2010","unstructured":"Asarin, E., Dang, T., Maler, O., Testylier, R.: Using redundant constraints for refinement. In: Bouajjani, A., Chin, W.-N. (eds.) ATVA 2010. LNCS, vol.\u00a06252, pp. 37\u201351. Springer, Heidelberg (2010)"},{"key":"30_CR5","volume-title":"Convex Analysis and Optimization","author":"D.P. Bertsekas","year":"2003","unstructured":"Bertsekas, D.P., Nedic, A., Ozdaglar, A.E.: Convex Analysis and Optimization. Athena Scientific, Belmont (2003)"},{"key":"30_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/3-540-48983-5_10","volume-title":"Hybrid Systems: Computation and Control","author":"A. Chutinan","year":"1999","unstructured":"Chutinan, A., Krogh, B.H.: Verification of polyhedral-invariant hybrid automata using polygonal flow pipe approximations. In: Vaandrager, F.W., van Schuppen, J.H. (eds.) HSCC 1999. LNCS, vol.\u00a01569, pp. 76\u201390. Springer, Heidelberg (1999)"},{"key":"30_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1007\/978-3-540-75596-8_30","volume-title":"Automated Technology for Verification and Analysis","author":"W. Damm","year":"2007","unstructured":"Damm, W., Disch, S., Hungar, H., Jacobs, S., Pang, J., Pigorsch, F., Scholl, C., Waldmann, U., Wirtz, B.: Exact state set representations in the verification of linear hybrid systems with large discrete state space. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol.\u00a04762, pp. 425\u2013440. Springer, Heidelberg (2007)"},{"key":"30_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-642-03845-7_9","volume-title":"Computational Methods in Systems Biology","author":"T. Dang","year":"2009","unstructured":"Dang, T., Le Guernic, C., Maler, O.: Computing reachable states for nonlinear biological models. In: Degano, P., Gorrieri, R. (eds.) CMSB 2009. LNCS, vol.\u00a05688, pp. 126\u2013141. Springer, Heidelberg (2009)"},{"key":"30_CR9","doi-asserted-by":"crossref","unstructured":"Frehse, G., Ray, R.: Design principles for an extendable verification tool for hybrid systems. In: ADHS (2009)","DOI":"10.3182\/20090916-3-ES-3003.00043"},{"key":"30_CR10","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.\u00a03927, pp. 257\u2013271. Springer, Heidelberg (2006)"},{"key":"30_CR11","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/s100090050008","volume":"1","author":"T. Henzinger","year":"1997","unstructured":"Henzinger, T., Ho, P.-H., Wong-Toi, H.: HyTech: A model checker for hybrid systems. Software Tools for Technology Transfer\u00a01, 110\u2013122 (1997)","journal-title":"Software Tools for Technology Transfer"},{"issue":"3b","key":"30_CR12","first-page":"347","volume":"9","author":"A. Kurzhanski","year":"2002","unstructured":"Kurzhanski, A., Varaiya, P.: Reachability analysis for uncertain systems\u2014the ellipsoidal technique. Dynamics of Continuous, Discrete and Impulsive Systems Series B: Applications and Algorithms\u00a09(3b), 347\u2013367 (2002)","journal-title":"Dynamics of Continuous, Discrete and Impulsive Systems Series B: Applications and Algorithms"},{"key":"30_CR13","unstructured":"Le Guernic, C.: Reachability analysis of hybrid systems with linear continuous dynamics. PhD thesis, Universit\u00e9 Grenoble 1 - Joseph Fourier (2009)"},{"key":"30_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"540","DOI":"10.1007\/978-3-642-02658-4_40","volume-title":"Computer Aided Verification","author":"C. Le Guernic","year":"2009","unstructured":"Le Guernic, C., Girard, A.: Reachability analysis of hybrid systems using support functions. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 540\u2013554. Springer, Heidelberg (2009)"},{"issue":"2","key":"30_CR15","first-page":"250","volume":"4","author":"C. Guernic Le","year":"2010","unstructured":"Le Guernic, C., Girard, A.: Reachability analysis of linear systems using support functions. Nonlinear Analysis: Hybrid Systems\u00a04(2), 250\u2013262 (2010)","journal-title":"Nonlinear Analysis: Hybrid Systems"},{"key":"30_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/978-3-642-00768-2_32","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C. Scholl","year":"2009","unstructured":"Scholl, C., Disch, S., Pigorsch, F., Kupferschmid, S.: Computing optimized representations for non-convex polyhedra by detection and removal of redundant linear constraints. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 383\u2013397. Springer, Heidelberg (2009)"},{"key":"30_CR17","volume-title":"Multivariable Feedback Control: Analysis and Design","author":"S. Skogestad","year":"2005","unstructured":"Skogestad, S., Postlethwaite, I.: Multivariable Feedback Control: Analysis and Design. John Wiley & Sons, Chichester (2005)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22110-1_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,12]],"date-time":"2019-06-12T13:41:00Z","timestamp":1560346860000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22110-1_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642221095","9783642221101"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22110-1_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}