{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,17]],"date-time":"2026-03-17T20:15:37Z","timestamp":1773778537740,"version":"3.50.1"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319406473","type":"print"},{"value":"9783319406480","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-40648-0_14","type":"book-chapter","created":{"date-parts":[[2016,6,3]],"date-time":"2016-06-03T09:42:13Z","timestamp":1464946933000},"page":"175-190","source":"Crossref","is-referenced-by-count":47,"title":["A Formally Verified Checker of the Safe Distance Traffic Rules for Autonomous Vehicles"],"prefix":"10.1007","author":[{"given":"Albert","family":"Rizaldi","sequence":"first","affiliation":[]},{"given":"Fabian","family":"Immler","sequence":"additional","affiliation":[]},{"given":"Matthias","family":"Althoff","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,6,4]]},"reference":[{"issue":"1","key":"14_CR1","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1080\/01441647.2014.997323","volume":"35","author":"K Aghabayk","year":"2015","unstructured":"Aghabayk, K., Sarvi, M., Young, W.: A state-of-the-art review of car-following models with particular considerations of heavy vehicles. Transport Rev. 35(1), 82\u2013105 (2015)","journal-title":"Transport Rev."},{"issue":"4","key":"14_CR2","doi-asserted-by":"crossref","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. Robot. 30(4), 903\u2013918 (2014)","journal-title":"IEEE Trans. Robot."},{"key":"14_CR3","unstructured":"American Prosecutors Research Institute: Crash Reconstruction Basics for Prosecutors: Targeting Hardcore Impaired Drivers. Author (2003)"},{"issue":"469067","key":"14_CR4","first-page":"13","volume":"2012","author":"C Chen","year":"2012","unstructured":"Chen, C., Liu, L., Du, X., Pei, Q., Zhao, X.: Improving driving safety based on safe distance design in vehicular sensor networks. Int. J. Distrib. Sens. Netw. 2012(469067), 13 (2012)","journal-title":"Int. J. Distrib. Sens. Netw."},{"key":"14_CR5","doi-asserted-by":"crossref","unstructured":"Eberl, M.: A decision procedure for univariate real polynomials in Isabelle\/HOL. In: Proceedings of the 2015 Conference on Certified Programs and Proofs. CPP 2015, Mumbai, India, pp. 75\u201383. ACM, New York (2015). http:\/\/doi.acm.org\/10.1145\/2676724.2693166","DOI":"10.1145\/2676724.2693166"},{"key":"14_CR6","unstructured":"Fricke, L.: Traffic Accident Reconstruction. The Traffic Accident Investigation Manual, vol. 2, Northwestern University Center for Public Safety (1990)"},{"issue":"2","key":"14_CR7","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1016\/0191-2615(81)90037-0","volume":"15","author":"P Gipps","year":"1981","unstructured":"Gipps, P.: A behavioural car-following model for computer simulation. Transp. Res. B Methodological 15(2), 105\u2013111 (1981)","journal-title":"Transp. Res. B Methodological"},{"key":"14_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"441","DOI":"10.1007\/978-3-642-38088-4_31","volume-title":"NASA Formal Methods","author":"AE Goodloe","year":"2013","unstructured":"Goodloe, A.E., Mu\u00f1oz, C., Kirchner, F., Correnson, L.: Verification of numerical programs: from real numbers to floating point numbers. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 441\u2013446. Springer, Heidelberg (2013)"},{"key":"14_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"100","DOI":"10.1007\/978-3-642-39634-2_10","volume-title":"Interactive Theorem Proving","author":"F Haftmann","year":"2013","unstructured":"Haftmann, F., Krauss, A., Kun\u010dar, O., Nipkow, T.: Data refinement in Isabelle\/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 100\u2013115. Springer, Heidelberg (2013)"},{"key":"14_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1007\/978-3-642-12251-4_9","volume-title":"Functional and Logic Programming","author":"F Haftmann","year":"2010","unstructured":"Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) FLOPS 2010. LNCS, vol. 6009, pp. 103\u2013117. Springer, Heidelberg (2010)"},{"key":"14_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1007\/978-3-540-74591-4_9","volume-title":"Theorem Proving in Higher Order Logics","author":"J Harrison","year":"2007","unstructured":"Harrison, J.: Verifying nonlinear real formulas via sums of squares. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 102\u2013118. Springer, Heidelberg (2007)"},{"key":"14_CR12","unstructured":"H\u00f6lzl, J.: Proving inequalities over reals with computation in Isabelle\/HOL. In: Proceedings of the ACM SIGSAM International Workshop on Programming Languages for Mechanized Mathematics Systems. pp. 38\u201345 (2009)"},{"key":"14_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1007\/978-3-662-46681-0_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F Immler","year":"2015","unstructured":"Immler, F.: Verified reachability analysis of continuous systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 37\u201351. Springer, Heidelberg (2015)"},{"issue":"3","key":"14_CR14","doi-asserted-by":"crossref","first-page":"804","DOI":"10.1109\/TVT.2011.2107584","volume":"60","author":"H Kowshik","year":"2011","unstructured":"Kowshik, H., Caveney, D., Kumar, P.: Provable systemwide safety in intelligent intersections. IEEE Trans. Veh. Technol. 60(3), 804\u2013818 (2011)","journal-title":"IEEE Trans. Veh. Technol."},{"key":"14_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"42","DOI":"10.1007\/978-3-642-21437-0_6","volume-title":"FM 2011: Formal Methods","author":"SM Loos","year":"2011","unstructured":"Loos, S.M., Platzer, A., Nistor, L.: Adaptive cruise control: hybrid, distributed, and now formally verified. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 42\u201356. Springer, Heidelberg (2011)"},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"Loos, S., Platzer, A.: Safe intersections: at the crossing of hybrid systems and verification. In: IEEE Conference on Intelligent Transportations Systems. pp. 1181\u20131186, October 2011","DOI":"10.1109\/ITSC.2011.6083138"},{"key":"14_CR17","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1007\/11532231_22","volume-title":"Automated Deduction \u2013 CADE-20","author":"S McLaughlin","year":"2005","unstructured":"McLaughlin, S., Harrison, J.V.: A proof-producing decision procedure for real arithmetic. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 295\u2013314. Springer, Heidelberg (2005)"},{"key":"14_CR18","volume-title":"Isabelle\/HOL - A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL - A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)"},{"key":"14_CR19","doi-asserted-by":"crossref","first-page":"15-1","DOI":"10.1201\/9780203490297.ch15","volume-title":"Handbook of Human Factors in Litigation","author":"RA Olsen","year":"2004","unstructured":"Olsen, R.A.: Pedestrian injury issues in litigation. In: Karwowski, W., Noy, Y.I. (eds.) Handbook of Human Factors in Litigation, pp. 15-1\u201315-23. CRC Press, Boca Raton (2004)"},{"key":"14_CR20","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-14509-4","volume-title":"Logical Analysis of Hybrid Systems","author":"A Platzer","year":"2010","unstructured":"Platzer, A.: Logical Analysis of Hybrid Systems. Springer, Heidelberg (2010)"},{"issue":"4","key":"14_CR21","first-page":"1","volume":"8","author":"A Platzer","year":"2012","unstructured":"Platzer, A.: A complete axiomatization of quantified differential dynamic logic for distributed hybrid systems. Logical Methods Comput. Sci. 8(4), 1\u201344 (2012)","journal-title":"Logical Methods Comput. Sci."},{"issue":"604023","key":"14_CR22","first-page":"7","volume":"2014","author":"D Qu","year":"2014","unstructured":"Qu, D., Chen, X., Yang, W., Bian, X.: Modeling of car-following required safe distance based on molecular dynamics. Math. Probl. Eng. 2014(604023), 7 (2014)","journal-title":"Math. Probl. Eng."},{"key":"14_CR23","doi-asserted-by":"crossref","unstructured":"Rizaldi, A., Althoff, M.: Formalising traffic rules for accountability of autonomous vehicles. In: IEEE Conference on Intelligent Transportation Systems. pp. 1658\u20131665 (2015)","DOI":"10.1109\/ITSC.2015.269"},{"issue":"1","key":"14_CR24","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1109\/TITS.2012.2225104","volume":"14","author":"B Vanholme","year":"2013","unstructured":"Vanholme, B., Gruyer, D., Lusetti, B., Glaser, S., Mammar, S.: Highly automated driving on highways based on legal safety. IEEE Trans. Intell. Transp. Syst. 14(1), 333\u2013347 (2013)","journal-title":"IEEE Trans. Intell. Transp. Syst."},{"key":"14_CR25","unstructured":"Wilson, B.H.: How soon to brake and how hard to brake: unified analysis of the envelope of opportunity for rear-end collision warnings. In: Enhanced Safety of Vehicles. vol. 47 (2001)"},{"issue":"10","key":"14_CR26","doi-asserted-by":"crossref","first-page":"1167","DOI":"10.1080\/00423110903365910","volume":"48","author":"L Xiao","year":"2010","unstructured":"Xiao, L., Gao, F.: A comprehensive review of the development of adaptive cruise control systems. Veh. Syst. Dyn. 48(10), 1167\u20131192 (2010)","journal-title":"Veh. Syst. Dyn."}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-40648-0_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T11:41:24Z","timestamp":1498304484000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-40648-0_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319406473","9783319406480"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-40648-0_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}