{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,19]],"date-time":"2026-02-19T04:26:46Z","timestamp":1771475206703,"version":"3.50.1"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030440503","type":"print"},{"value":"9783030440510","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","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":[[2020]]},"DOI":"10.1007\/978-3-030-44051-0_54","type":"book-chapter","created":{"date-parts":[[2020,5,7]],"date-time":"2020-05-07T16:02:40Z","timestamp":1588867360000},"page":"939-955","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Counterexample-Guided Safety Contracts for Autonomous Driving"],"prefix":"10.1007","author":[{"given":"Jonathan","family":"DeCastro","sequence":"first","affiliation":[]},{"given":"Lucas","family":"Liebenwein","sequence":"additional","affiliation":[]},{"given":"Cristian-Ioan","family":"Vasile","sequence":"additional","affiliation":[]},{"given":"Russ","family":"Tedrake","sequence":"additional","affiliation":[]},{"given":"Sertac","family":"Karaman","sequence":"additional","affiliation":[]},{"given":"Daniela","family":"Rus","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,5,8]]},"reference":[{"key":"54_CR1","unstructured":"Althoff, M.: An introduction to CORA 2015. In: Proceedings of the Workshop on Applied Verification for Continuous and Hybrid Systems, pp. 120\u2013151 (2015)"},{"key":"54_CR2","doi-asserted-by":"publisher","first-page":"903","DOI":"10.1109\/TRO.2014.2312453","volume":"30","author":"M Althoff","year":"2014","unstructured":"Althoff, M., Dolan, J.: Online verification of automated road vehicles using reachability analysis. IEEE Trans. Rob. 30, 903\u2013918 (2014)","journal-title":"IEEE Trans. Rob."},{"issue":"1","key":"54_CR3","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., Ho, P.H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theoret. Comput. Sci. 138(1), 3\u201334 (1995)","journal-title":"Theoret. Comput. Sci."},{"issue":"1","key":"54_CR4","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1145\/1132357.1132363","volume":"5","author":"R Alur","year":"2006","unstructured":"Alur, R., Dang, T., Ivan\u010di\u0107, F.: Predicate abstraction for reachability analysis of hybrid systems. ACM Trans. Embedded Comput. Syst. (TECS) 5(1), 152\u2013199 (2006)","journal-title":"ACM Trans. Embedded Comput. Syst. (TECS)"},{"key":"54_CR5","unstructured":"Baram, N., Anschel, O., Caspi, I., Mannor, S.: End-to-end differentiable adversarial imitation learning. In: ICML (2017)"},{"key":"54_CR6","volume-title":"Hybrid Systems: Computation and Control","author":"A Bhatia","year":"2004","unstructured":"Bhatia, A., Frazzoli, E.: Incremental search methods for reachability analysis of continuous and hybrid systems. In: Alur, R., Pappas, G.J. (eds.) Hybrid Systems: Computation and Control. Springer, Heidelberg (2004)"},{"issue":"6","key":"54_CR7","doi-asserted-by":"publisher","first-page":"1360","DOI":"10.2514\/1.G000774","volume":"40","author":"M Chen","year":"2017","unstructured":"Chen, M., Hu, Q., Fisac, J.F., Akametalu, K., Mackin, C., Tomlin, C.J.: Reachability-based safety and goal satisfaction of unmanned aerial platoons on air highways. J. Guid. Control Dynam. 40(6), 1360\u20131373 (2017)","journal-title":"J. Guid. Control Dynam."},{"key":"54_CR8","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 (2013)","DOI":"10.1007\/978-3-642-39799-8_18"},{"key":"54_CR9","doi-asserted-by":"crossref","unstructured":"Chen, X., Schupp, S., Makhlouf, I., \u00c1brah\u00e1m, E., Frehse, G., Kowalewski, S.: A benchmark suite for hybrid systems reachability analysis. In: NASA Formal Methods Symposium (2015)","DOI":"10.1007\/978-3-319-17524-9_29"},{"issue":"11\u201312","key":"54_CR10","doi-asserted-by":"publisher","first-page":"1232","DOI":"10.1177\/0278364908097582","volume":"27","author":"P Cheng","year":"2008","unstructured":"Cheng, P., Kumar, V.: Sampling-based falsification and verification of controllers for continuous dynamic systems. Int. J. Robot. Res. 27(11\u201312), 1232\u20131245 (2008)","journal-title":"Int. J. Robot. Res."},{"key":"54_CR11","doi-asserted-by":"crossref","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: International Conference on Computer Aided Verification (2000)","DOI":"10.1007\/10722167_15"},{"key":"54_CR12","unstructured":"Clarke, E., Grumberg, O., Long, D.: Verification tools for finite-state concurrent systems. In: Workshop\/School\/Symposium of the REX Project (Research and Education in Concurrent Systems) (1993)"},{"key":"54_CR13","unstructured":"Coulter, R.C.: Implementation of the pure pursuit path tracking algorithm. Technical report CMU-RI-TR-92-01, Carnegie Mellon University, Pittsburgh, PA (1992)"},{"key":"54_CR14","doi-asserted-by":"crossref","unstructured":"DeCastro, J.A., Kress-Gazit, H.: Nonlinear controller synthesis and automatic workspace partitioning for reactive high-level behaviors. In: ACM International Conference on Hybrid Systems: Computation and Control (HSCC), Vienna, Austria (2016)","DOI":"10.1145\/2883817.2883832"},{"key":"54_CR15","unstructured":"Economic Commission for Europe \u2013 Inland Transport Committee, Vienna, Austria: Convention on Road Traffic, E\/CONF.56\/16\/Rev.1\/Amend.1 edn. (1968)"},{"key":"54_CR16","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1109\/TITS.2015.2453404","volume":"17","author":"SM Erlien","year":"2016","unstructured":"Erlien, S.M., Fujita, S., Gerdes, J.C.: Shared steering control using safe envelopes for obstacle avoidance and vehicle stability. IEEE Trans. Intell. Transp. Syst. 17, 441\u2013451 (2016)","journal-title":"IEEE Trans. Intell. Transp. Syst."},{"key":"54_CR17","doi-asserted-by":"crossref","unstructured":"Fisac, J., Bajcsy, A., Herbert, S., Fridovich-Keil, D., Wang, S., Tomlin, C., Dragan, A.: Probabilistically safe robot planning with confidence-based human predictions. In: Proceedings of Robotics: Science and Systems, Pittsburgh, PA, June 2018","DOI":"10.15607\/RSS.2018.XIV.069"},{"issue":"1","key":"54_CR18","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1137\/S0036144504446096","volume":"47","author":"PE Gill","year":"2005","unstructured":"Gill, P.E., Murray, W., Saunders, M.A.: SNOPT: an SQP algorithm for large-scale constrained optimization. SIAM Rev. 47(1), 99\u2013131 (2005)","journal-title":"SIAM Rev."},{"key":"54_CR19","doi-asserted-by":"publisher","first-page":"338","DOI":"10.2514\/3.20223","volume":"10","author":"CR Hargraves","year":"1987","unstructured":"Hargraves, C.R., Paris, S.W.: Direct trajectory optimization using nonlinear programming and collocation. AIAA J. Guid. 10, 338\u2013342 (1987)","journal-title":"AIAA J. Guid."},{"key":"54_CR20","doi-asserted-by":"crossref","unstructured":"Ivanovic, B., Harrison, J., Sharma, A., Chen, M., Pavone, M.: BaRC: backward reachability curriculum for robotic reinforcement learning. \narXiv:1806.06161\n\n (2018)","DOI":"10.1109\/ICRA.2019.8794206"},{"key":"54_CR21","doi-asserted-by":"crossref","unstructured":"Kapinski, J., Deshmukh, J., Sankaranarayanan, S., Arechiga, N.: Simulation-guided Lyapunov analysis for hybrid dynamical systems. In: Proceedings of the International Conference on Hybrid Systems: Computation and Control (2014)","DOI":"10.1145\/2562059.2562139"},{"key":"54_CR22","doi-asserted-by":"crossref","unstructured":"Karlsson, J., Vasile, C.I., Tumova, J., Karaman, S., Rus, D.: Multi-vehicle motion planning for social optimal mobility-on-demand. In: IEEE International Conference on Robotics and Automation (ICRA), Brisbane, Australia (2018)","DOI":"10.1109\/ICRA.2018.8462968"},{"key":"54_CR23","doi-asserted-by":"crossref","unstructured":"Kim, E.S., Arcak, M., Seshia, S.A.: Compositional controller synthesis for vehicular traffic networks. In: IEEE Conference on Decision and Control (CDC), pp. 6165\u20136171 (2015)","DOI":"10.1109\/CDC.2015.7403189"},{"key":"54_CR24","doi-asserted-by":"crossref","unstructured":"Kim, E.S., Sadraddini, S., Belta, C., Arcak, M., Seshia, S.A.: Dynamic contracts for distributed temporal logic control of traffic networks. In: IEEE Conference on Decision and Control (CDC), pp. 3640\u20133645 (2017)","DOI":"10.1109\/CDC.2017.8264194"},{"key":"54_CR25","doi-asserted-by":"crossref","unstructured":"Kuefler, A., Morton, J., Wheeler, T.A., Kochenderfer, M.J.: Imitating driver behavior with generative adversarial networks. In: IEEE Intelligent Vehicles Symposium (IV), pp. 204\u2013211 (2017)","DOI":"10.1109\/IVS.2017.7995721"},{"key":"54_CR26","doi-asserted-by":"crossref","unstructured":"Liebenwein, L., Baykal, C., Gilitschenski, I., Karaman, S., Rus, D.: Sampling-based approximation algorithms for reachability analysis with provable guarantees. In: Proceedings of Robotics: Science and Systems, Pittsburgh, PA, June 2018","DOI":"10.15607\/RSS.2018.XIV.014"},{"key":"54_CR27","unstructured":"Liebenwein, L., Schwarting, W., Vasile, C.I., DeCastro, J., Alonso-Mora, J., Karaman, S., Rus, D.: Compositional and contract-based verification for autonomous driving on road networks. In: International Symposium on Robotics Research (ISRR) (2017)"},{"issue":"7","key":"54_CR28","doi-asserted-by":"publisher","first-page":"947","DOI":"10.1109\/TAC.2005.851439","volume":"50","author":"IM Mitchell","year":"2005","unstructured":"Mitchell, I.M., Bayen, A.M., Tomlin, C.J.: A time-dependent Hamilton-Jacobi formulation of reachable sets for continuous dynamic games. IEEE Trans. Autom. Control 50(7), 947\u2013957 (2005)","journal-title":"IEEE Trans. Autom. Control"},{"key":"54_CR29","doi-asserted-by":"crossref","unstructured":"Morton, J., Kochenderfer, M.J.: Simultaneous policy learning and latent state inference for imitating driver behavior. In: IEEE International Conference on Intelligent Transportation Systems (ITSC), pp. 1\u20136 (2017)","DOI":"10.1109\/ITSC.2017.8317738"},{"key":"54_CR30","doi-asserted-by":"crossref","unstructured":"Plaku, E., Kavraki, L., Vardi, M.: Falsification of LTL safety properties in hybrid systems. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems (2009)","DOI":"10.1007\/978-3-642-00768-2_31"},{"key":"54_CR31","doi-asserted-by":"crossref","unstructured":"Sangiovanni-Vincentelli, A., Damm, W., Passerone, R.: Taming Dr. Frankenstein: contract-based design for cyber-physical systems. In: 2011 Control and Decision Conference and European Control Conference (2012)","DOI":"10.3166\/ejc.18.217-238"},{"key":"54_CR32","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Fainekos, G.: Falsification of temporal properties of hybrid systems using the cross-entropy method. In: ACM International Conference on Hybrid Systems: Computation and Control, pp. 125\u2013134 (2012)","DOI":"10.1145\/2185632.2185653"},{"key":"54_CR33","doi-asserted-by":"crossref","unstructured":"Schwarting, W., Alonso-Mora, J., Paull, L., Karaman, S., Rus, D.: Parallel autonomy in automated vehicles: safe motion generation with minimal intervention. In: IEEE International Conference on Robotics and Automation (ICRA) (2017)","DOI":"10.1109\/ICRA.2017.7989224"},{"key":"54_CR34","unstructured":"Shalev-Shwartz, S., Shammah, S., Shashua, A.: Safe, multi-agent, reinforcement learning for autonomous driving. CoRR abs\/1610.03295 (2016)"},{"key":"54_CR35","unstructured":"Russ Tedrake and the Drake Development Team: Drake: A planning, control, and analysis toolbox for nonlinear dynamical systems (2016). \nhttp:\/\/drake.mit.edu"},{"key":"54_CR36","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32460-4","volume-title":"Traffic Flow Dynamics","author":"M Treiber","year":"2013","unstructured":"Treiber, M., Kesting, A.: Traffic Flow Dynamics. Springer, Heidelberg (2013)"},{"key":"54_CR37","doi-asserted-by":"crossref","unstructured":"Vasile, C.I., Tumova, J., Karaman, S., Belta, C., Rus, D.: Minimum-violation scLTL motion planning for mobility-on-demand. In: IEEE International Conference on Robotics and Automation (ICRA), Singapore, pp. 1481\u20131488 (2017)","DOI":"10.1109\/ICRA.2017.7989177"},{"key":"54_CR38","doi-asserted-by":"crossref","unstructured":"Wongpiromsarn, T., Topcu, U., Murray, R.M.: Receding horizon temporal logic planning for dynamical systems. In: IEEE Conference on Decision and Control (CDC) and Chinese Control Conference, pp. 5997\u20136004 (2009)","DOI":"10.1109\/CDC.2009.5399536"}],"container-title":["Springer Proceedings in Advanced Robotics","Algorithmic Foundations of Robotics XIII"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-44051-0_54","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,7]],"date-time":"2020-05-07T16:11:34Z","timestamp":1588867894000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-44051-0_54"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030440503","9783030440510"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-44051-0_54","relation":{},"ISSN":["2511-1256","2511-1264"],"issn-type":[{"value":"2511-1256","type":"print"},{"value":"2511-1264","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"8 May 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"WAFR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Workshop on the Algorithmic Foundations of Robotics","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Merida","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Mexico","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 December 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 December 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"wafr2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/parasol.tamu.edu\/wafr\/wafr2018\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}