{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,11]],"date-time":"2025-11-11T12:08:41Z","timestamp":1762862921525,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662545768"},{"type":"electronic","value":"9783662545775"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-662-54577-5_32","type":"book-chapter","created":{"date-parts":[[2017,3,30]],"date-time":"2017-03-30T10:48:06Z","timestamp":1490870886000},"page":"555-572","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Rigorous Simulation-Based Analysis of Linear Hybrid Systems"],"prefix":"10.1007","author":[{"given":"Stanley","family":"Bak","sequence":"first","affiliation":[]},{"given":"Parasara Sridhar","family":"Duggirala","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,3,31]]},"reference":[{"key":"32_CR1","unstructured":"Computer Assisted Proofs in Dynamic Groups (CAPD). http:\/\/capd.ii.uj.edu.pl\/index.php"},{"key":"32_CR2","unstructured":"Althoff, M.: An introduction to CORA. In: Proceedings of the Workshop on Applied Verification for Continuous and Hybrid Systems (2015)"},{"key":"32_CR3","doi-asserted-by":"crossref","unstructured":"Althoff, M., Krogh, B.H.: Avoiding geometric intersection operations in reachability analysis of hybrid systems. In: Hybrid Systems: Computation and Control, pp. 45\u201354 (2012)","DOI":"10.1145\/2185632.2185643"},{"key":"32_CR4","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. Theoret. Comput. Sci. 138, 3\u201334 (1995)","journal-title":"Theoret. Comput. Sci."},{"key":"32_CR5","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126, 183\u2013235 (1994)","journal-title":"Theoret. Comput. Sci."},{"key":"32_CR6","doi-asserted-by":"crossref","unstructured":"Bak, S., Bogomolov, S., Henzinger, T.A., Johnson, T.T., Prakash, P.: Scalable static hybridization methods for analysis of nonlinear systems. In: Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, HSCC 2016, pp. 155\u2013164. ACM, New York (2016)","DOI":"10.1145\/2883817.2883837"},{"key":"32_CR7","doi-asserted-by":"crossref","unstructured":"Bak, S., Bogomolov, S., Johnson, T.T.: HYST: a source transformation and translation tool for hybrid automaton models. In: 18th International Conference on Hybrid Systems: Computation and Control, Seattle, Washington. ACM, April 2015","DOI":"10.1145\/2728606.2728630"},{"key":"32_CR8","unstructured":"Bak, S., Bogomolov, S., Schilling, C.: High-level hybrid systems analysis with hypy. In: ARCH 2016: Proceedings of the 3rd Workshop on Applied Verification for Continuous and Hybrid Systems (2016)"},{"key":"32_CR9","doi-asserted-by":"crossref","unstructured":"Balkan, A., Tabuada, P., Deshmukh, J.V., Jin, X., Kapinski, J.: Underminer: a framework for automatically identifying non-converging behaviors in black box system models. In: Proceedings of the 13th International Conference on Embedded Software, p. 7. ACM (2016)","DOI":"10.1145\/2968478.2968487"},{"key":"32_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/BFb0020949","volume-title":"Hybrid Systems III","author":"J Bengtsson","year":"1996","unstructured":"Bengtsson, J., Larsen, K., Larsson, F., Pettersson, P., Yi, W.: UPPAAL\u2014a tool suite for automatic verification of real-time systems. In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds.) HS 1995. LNCS, vol. 1066, pp. 232\u2013243. Springer, Heidelberg (1996). doi:10.1007\/BFb0020949"},{"key":"32_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"535","DOI":"10.1007\/978-3-642-27549-4_69","volume-title":"Computer Aided Systems Theory \u2013 EUROCAST 2011","author":"X Chen","year":"2012","unstructured":"Chen, X., \u00c1brah\u00e1m, E.: Choice of directions for the approximation of reachable sets for hybrid systems. In: Moreno-D\u00edaz, R., Pichler, F., Quesada-Arencibia, A. (eds.) EUROCAST 2011. LNCS, vol. 6927, pp. 535\u2013542. Springer, Heidelberg (2012). doi:10.1007\/978-3-642-27549-4_69"},{"key":"32_CR12","doi-asserted-by":"crossref","unstructured":"Chen, X., Abraham, E., Sankaranarayanan, S.: Taylor model flowpipe construction for non-linear hybrid systems. In: 2013 IEEE 34th Real-Time Systems Symposium, pp. 183\u2013192 (2012)","DOI":"10.1109\/RTSS.2012.70"},{"issue":"1","key":"32_CR13","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1109\/TAC.2002.806655","volume":"48","author":"A Chutinan","year":"2003","unstructured":"Chutinan, A., Krogh, B.H.: Computational techniques for hybrid system verification. IEEE Trans. Autom. Control 48(1), 64\u201375 (2003)","journal-title":"IEEE Trans. Autom. Control"},{"key":"32_CR14","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. 5688, pp. 126\u2013141. Springer, Heidelberg (2009). doi:10.1007\/978-3-642-03845-7_9"},{"key":"32_CR15","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":"32_CR16","doi-asserted-by":"crossref","unstructured":"Duggirala, P.S., Mitra, S., Viswanathan, M.: Verification of annotated models from executions. In: Proceedings of the 13th International Conference on Embedded Software (EMSOFT), Montreal, Canada (2013)","DOI":"10.1109\/EMSOFT.2013.6658604"},{"key":"32_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/978-3-662-46681-0_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"PS Duggirala","year":"2015","unstructured":"Duggirala, P.S., Mitra, S., Viswanathan, M., Potok, M.: C2E2: a verification tool for stateflow models. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 68\u201382. Springer, Heidelberg (2015). doi:10.1007\/978-3-662-46681-0_5"},{"key":"32_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/978-3-319-41528-4_26","volume-title":"Computer Aided Verification","author":"PS Duggirala","year":"2016","unstructured":"Duggirala, P.S., Viswanathan, M.: Parsimonious, simulation based verification of linear systems. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 477\u2013494. Springer, Heidelberg (2016). doi:10.1007\/978-3-319-41528-4_26"},{"issue":"42","key":"32_CR19","doi-asserted-by":"publisher","first-page":"4262","DOI":"10.1016\/j.tcs.2009.06.021","volume":"410","author":"GE Fainekos","year":"2009","unstructured":"Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications for continuous-time signals. Theoret. Comput. Sci. 410(42), 4262\u20134291 (2009)","journal-title":"Theoret. Comput. Sci."},{"key":"32_CR20","doi-asserted-by":"crossref","unstructured":"Fan, C., Kapinski, J., Jin, X., Mitra, S.: Locally optimal reach set over-approximation for nonlinear systems. In: Proceedings of the 13th International Conference on Embedded Software, p. 6. ACM (2016)","DOI":"10.1145\/2968478.2968482"},{"key":"32_CR21","doi-asserted-by":"crossref","unstructured":"Frehse, G.: PHAVer: algorithmic verification of hybrid systems past hytech. In: HSCC, pp. 258\u2013273 (2005)","DOI":"10.1007\/978-3-540-31954-2_17"},{"key":"32_CR22","doi-asserted-by":"crossref","unstructured":"Frehse, G., Kateja, R., Le Guernic, C.: Flowpipe approximation, clustering in space-time. In: Proceedings of Hybrid Systems: Computation and Control (HSCC 2013), pp. 203\u2013212. ACM (2013)","DOI":"10.1145\/2461328.2461361"},{"key":"32_CR23","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., Le 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":"32_CR24","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, Heidelberg (2015). doi:10.1007\/978-3-319-21401-6_36"},{"key":"32_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/978-3-540-31954-2_19","volume-title":"Hybrid Systems: Computation and Control","author":"A Girard","year":"2005","unstructured":"Girard, A.: Reachability of uncertain linear systems using zonotopes. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 291\u2013305. Springer, Heidelberg (2005). doi:10.1007\/978-3-540-31954-2_19"},{"key":"32_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"460","DOI":"10.1007\/3-540-63166-6_48","volume-title":"Computer Aided Verification","author":"TA Henzinger","year":"1997","unstructured":"Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: HyTech: a model checker for hybrid systems. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 460\u2013463. Springer, Heidelberg (1997). doi:10.1007\/3-540-63166-6_48"},{"key":"32_CR27","unstructured":"Lagerberg, A.: A benchmark on hybrid control of an automotive powertrain with backlash. Technical report (2007)"},{"key":"32_CR28","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. 5643, pp. 540\u2013554. Springer, Heidelberg (2009). doi:10.1007\/978-3-642-02658-4_40"},{"key":"32_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/BFb0032003","volume-title":"Real-Time: Theory in Practice","author":"O Maler","year":"1992","unstructured":"Maler, O., Manna, Z., Pnueli, A.: Prom timed to hybrid systems. In: Bakker, J.W., Huizing, C., Roever, W.P., Rozenberg, G. (eds.) REX 1991. LNCS, vol. 600, pp. 447\u2013484. Springer, Heidelberg (1992). doi:10.1007\/BFb0032003"},{"key":"32_CR30","doi-asserted-by":"crossref","unstructured":"Nghiem, T., Sankaranarayanan, S., Fainekos, G., Ivanci\u0107, F., Gupta, A., Pappas, G.J.: Monte-Carlo techniques for falsification of temporal properties of non-linear hybrid systems. In: 2010 Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, pp. 211\u2013220. ACM (2010)","DOI":"10.1145\/1755952.1755983"},{"issue":"2","key":"32_CR31","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."}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-54577-5_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,21]],"date-time":"2021-04-21T02:43:41Z","timestamp":1618973021000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-54577-5_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783662545768","9783662545775"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-54577-5_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"31 March 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Uppsala","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Sweden","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 April 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 April 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.etaps.org\/index.php\/2017\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}