{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T14:51:31Z","timestamp":1777387891670,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642214363","type":"print"},{"value":"9783642214370","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-21437-0_6","type":"book-chapter","created":{"date-parts":[[2011,6,18]],"date-time":"2011-06-18T03:33:16Z","timestamp":1308367996000},"page":"42-56","source":"Crossref","is-referenced-by-count":87,"title":["Adaptive Cruise Control: Hybrid, Distributed, and Now Formally Verified"],"prefix":"10.1007","author":[{"given":"Sarah M.","family":"Loos","sequence":"first","affiliation":[]},{"given":"Andr\u00e9","family":"Platzer","sequence":"additional","affiliation":[]},{"given":"Ligia","family":"Nistor","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"6_CR1","unstructured":"Chang, J., Cohen, D., Blincoe, L., Subramanian, R., Lombardo, L.: CICAS-V research on comprehensive costs of intersection crashes. Technical Report 07-0016, NHTSA (2007)"},{"key":"6_CR2","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1080\/00207170600587531","volume":"79","author":"W. Damm","year":"2006","unstructured":"Damm, W., Hungar, H., Olderog, E.R.: Verification of cooperating traffic agents. International Journal of Control\u00a079, 395\u2013421 (2006)","journal-title":"International Journal of Control"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"Dao, T.S., Clark, C.M., Huissoon, J.P.: Distributed platoon assignment and lane selection for traffic flow optimization. In: IEEE IV 2008, pp. 739\u2013744 (2008)","DOI":"10.1109\/IVS.2008.4621202"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"Dao, T.S., Clark, C.M., Huissoon, J.P.: Optimized lane assignment using inter-vehicle communication. In: IEEE IV 2007, pp. 1217\u20131222 (2007)","DOI":"10.1109\/IVS.2007.4290284"},{"key":"6_CR5","unstructured":"Hall, R., Chin, C., Gadgil, N.: The automated highway system \/ street interface: Final report. PATH Research Report UCB-ITS-PRR-2003-06, UC Berkeley (2003)"},{"key":"6_CR6","unstructured":"Hall, R., Chin, C.: Vehicle sorting for platoon formation: Impacts on highway entry and troughput. PATH Research Report UCB-ITS-PRR-2002-07, UC Berkeley (2002)"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"Hsu, A., Eskafi, F., Sachs, S., Varaiya, P.: Design of platoon maneuver protocols for IVHS. PATH Research Report UCB-ITS-PRR-91-6, UC Berkeley (1991)","DOI":"10.23919\/ACC.1991.4791861"},{"key":"6_CR8","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-4573-3","volume-title":"Automated Highway Systems","author":"P.A. Ioannou","year":"1997","unstructured":"Ioannou, P.A.: Automated Highway Systems. Springer, Heidelberg (1997)"},{"key":"6_CR9","unstructured":"Jula, H., Kosmatopoulos, E.B., Ioannou, P.A.: Collision avoidance analysis for lane changing and merging. PATH Research Report UCB-ITS-PRR-99-13, UC Berkeley (1999)"},{"key":"6_CR10","unstructured":"Horowitz, R., Tan, C.W., Sun, X.: An efficient lane change maneuver for platoons of vehicles in an automated highway system. PATH Research Report UCB-ITS-PRR-2004-16, UC Berkeley (2004)"},{"key":"6_CR11","unstructured":"Shladover, S.E.: Effects of traffic density on communication requirements for Cooperative Intersection Collision Avoidance Systems (CICAS). PATH Working Paper UCB-ITS-PWP-2005-1, UC Berkeley (2004)"},{"key":"6_CR12","doi-asserted-by":"publisher","first-page":"1269","DOI":"10.1016\/j.conengprac.2004.04.002","volume":"38","author":"O. Stursberg","year":"2004","unstructured":"Stursberg, O., Fehnker, A., Han, Z., Krogh, B.H.: Verification of a cruise control system using counterexample-guided search. Control Engineering Practice\u00a038, 1269\u20131278 (2004)","journal-title":"Control Engineering Practice"},{"key":"6_CR13","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1109\/9.250509","volume":"38","author":"P. Varaiya","year":"1993","unstructured":"Varaiya, P.: Smart cars on smart roads: problems of control. IEEE Trans. Automat. Control\u00a038, 195\u2013207 (1993)","journal-title":"IEEE Trans. Automat. Control"},{"key":"6_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1007\/978-3-642-00602-9_28","volume-title":"Hybrid Systems: Computation and Control","author":"T. Wongpiromsarn","year":"2009","unstructured":"Wongpiromsarn, T., Mitra, S., Murray, R.M., Lamperski, A.: Periodically controlled hybrid systems: Verifying a controller for an autonomous vehicle. In: Majumdar, R., Tabuada, P. (eds.) HSCC 2009. LNCS, vol.\u00a05469, pp. 396\u2013410. Springer, Heidelberg (2009)"},{"key":"6_CR15","unstructured":"Chee, W., Tomizuka, M.: Vehicle lane change maneuver in automated highway systems. PATH Research Report UCB-ITS-PRR-94-22, UC Berkeley (1994)"},{"key":"6_CR16","unstructured":"Johansson, R., Rantzer, A. (eds.): Nonlinear and Hybrid Systems in Automotive Control. Society of Automotive Engineers Inc. (2003)"},{"key":"6_CR17","doi-asserted-by":"crossref","unstructured":"Althoff, M., Althoff, D., Wollherr, D., Buss, M.: Safety verification of autonomous vehicles for coordinated evasive maneuvers. In: IEEE IV 2010, pp. 1078\u20131083 (2010)","DOI":"10.1109\/IVS.2010.5548121"},{"key":"6_CR18","first-page":"335","volume-title":"Nonlinear and Hybrid Systems in Automotive Control","author":"L. Berardi","year":"2003","unstructured":"Berardi, L., Santis, E., Benedetto, M., Pola, G.: Approximations of maximal controlled safe sets for hybrid systems. In: Johansson, R., Rantzer, A. (eds.) Nonlinear and Hybrid Systems in Automotive Control, pp. 335\u2013350. Springer, Heidelberg (2003)"},{"key":"6_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1007\/978-3-642-15205-4_36","volume-title":"Computer Science Logic","author":"A. Platzer","year":"2010","unstructured":"Platzer, A.: Quantified Differential Dynamic Logic for Distributed Hybrid Systems. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol.\u00a06247, pp. 469\u2013483. Springer, Heidelberg (2010)"},{"key":"6_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/3-540-64358-3_45","volume-title":"Hybrid Systems: Computation and Control","author":"J. Lygeros","year":"1998","unstructured":"Lygeros, J., Lynch, N.: Strings of vehicles: Modeling safety conditions. In: Henzinger, T.A., Sastry, S.S. (eds.) HSCC 1998. LNCS, vol.\u00a01386, pp. 273\u2013288. Springer, Heidelberg (1998)"},{"key":"6_CR21","first-page":"154","volume-title":"HART","author":"E. Dolginova","year":"1997","unstructured":"Dolginova, E., Lynch, N.: Safety verification for automated platoon maneuvers: A case study. In: Maler, O. (ed.) HART, pp. 154\u2013170. Springer, Heidelberg (1997)"},{"key":"6_CR22","unstructured":"Electronic Proof and Demo, http:\/\/www.ls.cs.cmu.edu\/dccs\/"},{"key":"6_CR23","doi-asserted-by":"crossref","unstructured":"Loos, S.M., Platzer, A., Nistor, L.: Adaptive cruise control: Hybrid, distributed, and now formally verified. Technical Report CMU-CS-11-107, Carnegie Mellon University (2011)","DOI":"10.1007\/978-3-642-21437-0_6"},{"key":"6_CR24","unstructured":"Germann, S.: Modellbildung und Modellgest\u00fctzte Regelung der Fahrzeugl\u00e4ngsdynamik. Fortschrittsberichte VDI, Reihe 12, Nr. 309, VDI Verlag (1997)"}],"container-title":["Lecture Notes in Computer Science","FM 2011: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-21437-0_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,11]],"date-time":"2019-06-11T20:07:13Z","timestamp":1560283633000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-21437-0_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642214363","9783642214370"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-21437-0_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}