{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,24]],"date-time":"2026-03-24T15:20:05Z","timestamp":1774365605257,"version":"3.50.1"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319633862","type":"print"},{"value":"9783319633879","type":"electronic"}],"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-319-63387-9_22","type":"book-chapter","created":{"date-parts":[[2017,7,12]],"date-time":"2017-07-12T08:53:43Z","timestamp":1499849623000},"page":"441-461","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":68,"title":["DryVR: Data-Driven Verification and Compositional Reasoning for Automotive Systems"],"prefix":"10.1007","author":[{"given":"Chuchu","family":"Fan","sequence":"first","affiliation":[]},{"given":"Bolun","family":"Qi","sequence":"additional","affiliation":[]},{"given":"Sayan","family":"Mitra","sequence":"additional","affiliation":[]},{"given":"Mahesh","family":"Viswanathan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,7,13]]},"reference":[{"key":"22_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/3-540-36577-X_15","volume-title":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"R Alur","year":"2003","unstructured":"Alur, R., Dang, T., Ivan\u010di\u0107, F.: Counter-example guided predicate abstraction of hybrid systems. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 208\u2013223. Springer, Heidelberg (2003)"},{"key":"22_CR2","doi-asserted-by":"crossref","unstructured":"Annapureddy, Y., Liu, C., Fainekos, G., Sankaranarayanan, S.: S-taliro: a tool for temporal logic falsification for hybrid systems. In: Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (2011)","DOI":"10.1007\/978-3-642-19835-9_21"},{"key":"22_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/3-540-45657-0_30","volume-title":"Computer Aided Verification","author":"E Asarin","year":"2002","unstructured":"Asarin, E., Dang, T., Maler, O.: The d\/dt tool for verification of hybrid systems. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 365\u2013370. Springer, Heidelberg (2002). doi:10.1007\/3-540-45657-0_30"},{"key":"22_CR4","unstructured":"Balluchi, A., Casagrande, A., Collins, P., Ferrari, A., Villa, T., Sangiovanni-Vincentelli, A.L.: Ariadne: a framework for reachability analysis of hybrid automata. In: Proceedings of the International Syposium on Mathematical Theory of Networks and Systems. Citeseer (2006)"},{"key":"22_CR5","doi-asserted-by":"crossref","unstructured":"Bogomolov, S., Frehse, G., Greitschus, M., Grosu, R., Pasareanu, C.S., Podelski, A., Strump, T.: Assume-guarantee abstraction refinement meets hybrid systems. In: 10th International Haifa Verification Conference, pp. 116\u2013131 (2014)","DOI":"10.1007\/978-3-319-13338-6_10"},{"key":"22_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1007\/3-540-56496-9_24","volume-title":"Computer Aided Verification","author":"K \u010cer\u0101ns","year":"1993","unstructured":"\u010cer\u0101ns, K.: Decidability of bisimulation equivalences for parallel timer processes. In: von Bochmann, G., Probst, D.K. (eds.) CAV 1992. LNCS, vol. 663, pp. 302\u2013315. Springer, Heidelberg (1993). doi:10.1007\/3-540-56496-9_24"},{"key":"22_CR7","doi-asserted-by":"crossref","unstructured":"Chen, X., \u00c1brah\u00e1m, E., Sankaranarayanan, S.: Flow*: an analyzer for non-linear hybrid systems. In: International Conference on Computer Aided Verification, pp. 258\u2013263 (2013)","DOI":"10.1007\/978-3-642-39799-8_18"},{"key":"22_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1007\/3-540-36577-X_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Clarke","year":"2003","unstructured":"Clarke, E., Fehnker, A., Han, Z., Krogh, B., Stursberg, O., Theobald, M.: Verification of hybrid systems based on counterexample-guided abstraction refinement. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 192\u2013207. Springer, Heidelberg (2003). doi:10.1007\/3-540-36577-X_14"},{"key":"22_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). doi:10.1007\/978-3-540-78800-3_24"},{"key":"22_CR10","doi-asserted-by":"crossref","unstructured":"Deng, Y., Rajhans, A., Julius, A.A.: Strong: a trajectory-based verification toolbox for hybrid systems. In: International Conference on Quantitative Evaluation of SysTems, pp. 165\u2013168 (2013)","DOI":"10.1007\/978-3-642-40196-1_13"},{"key":"22_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-642-14295-6_17","volume-title":"Computer Aided Verification","author":"A Donz\u00e9","year":"2010","unstructured":"Donz\u00e9, A.: Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 167\u2013170. Springer, Heidelberg (2010). doi:10.1007\/978-3-642-14295-6_17"},{"key":"22_CR12","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":"22_CR13","unstructured":"Duggirala, P.S.: Dynamic analysis of cyber-physical systems. Ph.D. thesis, University of Illinois at Urbana-Champaign (2015)"},{"key":"22_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"536","DOI":"10.1007\/978-3-319-21690-4_37","volume-title":"Computer Aided Verification","author":"PS Duggirala","year":"2015","unstructured":"Duggirala, P.S., Fan, C., Mitra, S., Viswanathan, M.: Meeting a powertrain verification challenge. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 536\u2013543. Springer, Cham (2015). doi:10.1007\/978-3-319-21690-4_37"},{"key":"22_CR15","doi-asserted-by":"crossref","unstructured":"Duggirala, P.S., Mitra, S., Viswanathan, M.: Verification of annotated models from executions. In: Proceedings of International Conference on Embedded Software (EMSOFT 2013), Montreal, QC, Canada, pp. 1\u201310. ACM SIGBED, IEEE, September 2013","DOI":"10.1109\/EMSOFT.2013.6658604"},{"key":"22_CR16","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":"22_CR17","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. Theor. Comput. Sci. 410, 4262\u20134291 (2009)","journal-title":"Theor. Comput. Sci."},{"key":"22_CR18","unstructured":"Fan, C., Duggirala, P.S., Mitra, S., Viswanathan, M.: Progress on powertrain verification challenge with C2E2. In: Workshop on Applied Verification for Continuous and Hybrid Systems (ARCH 2015) (2015)"},{"key":"22_CR19","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 ACM-SIGBED International Conference on Embedded Software (EMSOFT), EMSOFT 2016, pp. 6:1\u20136:10. ACM, New York (2016)","DOI":"10.1145\/2968478.2968482"},{"key":"22_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"446","DOI":"10.1007\/978-3-319-24953-7_32","volume-title":"Automated Technology for Verification and Analysis","author":"C Fan","year":"2015","unstructured":"Fan, C., Mitra, S.: Bounded verification with on-the-fly discrepancy computation. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) ATVA 2015. LNCS, vol. 9364, pp. 446\u2013463. Springer, Cham (2015). doi:10.1007\/978-3-319-24953-7_32"},{"key":"22_CR21","doi-asserted-by":"crossref","unstructured":"Fan, C., Qi, B., Mitra, S., Viswanathan, M.: DRYVR: data-driven verification and compositional reasoning for automotive systems. arXiv preprint arXiv:1702.06902 (2017)","DOI":"10.1007\/978-3-319-63387-9_22"},{"key":"22_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"531","DOI":"10.1007\/978-3-319-41528-4_29","volume-title":"Computer Aided Verification","author":"C Fan","year":"2016","unstructured":"Fan, C., Qi, B., Mitra, S., Viswanathan, M., Duggirala, P.S.: Automatic reachability analysis for nonlinear hybrid models with C2E2. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 531\u2013538. Springer, Cham (2016). doi:10.1007\/978-3-319-41528-4_29"},{"key":"22_CR23","unstructured":"Finley, T.: Python package PyGLPK. http:\/\/tfinley.net\/software\/pyglpk\/"},{"key":"22_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-540-31954-2_17","volume-title":"Hybrid Systems: Computation and Control","author":"G Frehse","year":"2005","unstructured":"Frehse, G.: PHAVer: algorithmic verification of hybrid systems past HyTech. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 258\u2013273. Springer, Heidelberg (2005). doi:10.1007\/978-3-540-31954-2_17"},{"key":"22_CR25","doi-asserted-by":"crossref","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: International Conference on Computer Aided Verification, pp. 379\u2013395. Springer (2011)","DOI":"10.1007\/978-3-642-22110-1_30"},{"key":"22_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/11730637_22","volume-title":"Hybrid Systems: Computation and Control","author":"A Girard","year":"2006","unstructured":"Girard, A., Pappas, G.J.: Verification using simulation. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol. 3927, pp. 272\u2013286. Springer, Heidelberg (2006). doi:10.1007\/11730637_22"},{"issue":"1","key":"22_CR27","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1109\/TAC.2009.2034922","volume":"55","author":"A Girard","year":"2010","unstructured":"Girard, A., Pola, G., Tabuada, P.: Approximately bisimilar symbolic models for incrementally stable switched systems. IEEE Trans. Autom. Contr. 55(1), 116\u2013126 (2010)","journal-title":"IEEE Trans. Autom. Contr."},{"key":"22_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/3-540-60472-3_14","volume-title":"Hybrid Systems II","author":"TA Henzinger","year":"1995","unstructured":"Henzinger, T.A., Ho, P.-H.: HyTech: the cornell hybrid technology tool. In: Antsaklis, P., Kohn, W., Nerode, A., Sastry, S. (eds.) HS 1994. LNCS, vol. 999, pp. 265\u2013293. Springer, Heidelberg (1995). doi:10.1007\/3-540-60472-3_14"},{"key":"22_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1007\/978-3-319-08867-9_25","volume-title":"Computer Aided Verification","author":"Z Huang","year":"2014","unstructured":"Huang, Z., Fan, C., Mereacre, A., Mitra, S., Kwiatkowska, M.: Invariant verification of nonlinear hybrid automata networks of cardiac cells. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 373\u2013390. Springer, Cham (2014). doi:10.1007\/978-3-319-08867-9_25"},{"key":"22_CR30","doi-asserted-by":"crossref","unstructured":"Jin, X., Deshmukh, J.V., Kapinski, J., Ueda, K., Butts, K.: Powertrain control verification benchmark. In: Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control, pp. 253\u2013262. ACM (2014)","DOI":"10.1145\/2562059.2562140"},{"key":"22_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"430","DOI":"10.1007\/978-3-642-02658-4_33","volume-title":"Computer Aided Verification","author":"A Kanade","year":"2009","unstructured":"Kanade, A., Alur, R., Ivan\u010di\u0107, F., Ramesh, S., Sankaranarayanan, S., Shashidhar, K.C.: Generating and analyzing symbolic traces of Simulink\/Stateflow models. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 430\u2013445. Springer, Heidelberg (2009). doi:10.1007\/978-3-642-02658-4_33"},{"key":"22_CR32","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/3897.001.0001","volume-title":"An Introduction to Computational Learning Theory","author":"MJ Kearns","year":"1994","unstructured":"Kearns, M.J., Vazirani, U.V.: An Introduction to Computational Learning Theory. MIT Press, Cambridge (1994)"},{"key":"22_CR33","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"},{"key":"22_CR34","unstructured":"Mathworks: Modeling an Automatic Transmission and Controller. http:\/\/www.mathworks.com\/videos\/modeling-an-automatic-transmission-and-controller-68823.html"},{"key":"22_CR35","unstructured":"Mathworks. Simple 2D Kinematic Vehicle Steering Model and Animation. https:\/\/www.mathworks.com\/matlabcentral\/fileexchange\/54852-simple-2d-kinematic-vehicle-steering-model-and-animation?requestedDomain=www.mathworks.com"},{"key":"22_CR36","doi-asserted-by":"crossref","unstructured":"O\u2019Kelly, M., Abbas, H., Gao, S., Shiraishi, S., Kato, S., Mangharam, R.: APEX: autonomous vehicle plan verification and execution (2016)","DOI":"10.4271\/2016-01-0019"},{"key":"22_CR37","doi-asserted-by":"crossref","unstructured":"Ouaknine, J., Worrell, J.: On the language inclusion problem for timed automata: closing a decidability gap. In: Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, pp. 54\u201363. IEEE (2004)","DOI":"10.1109\/LICS.2004.1319600"},{"key":"22_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1007\/978-3-662-49674-9_48","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N Roohi","year":"2016","unstructured":"Roohi, N., Prabhakar, P., Viswanathan, M.: Hybridization based CEGAR for hybrid automata with affine dynamics. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 752\u2013769. Springer, Heidelberg (2016). doi:10.1007\/978-3-662-49674-9_48"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63387-9_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,13]],"date-time":"2021-07-13T00:23:25Z","timestamp":1626135805000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-63387-9_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319633862","9783319633879"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63387-9_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"13 July 2017","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":"Heidelberg","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","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 July 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 July 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/cavconference.org\/2017\/","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"}]}}