{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,14]],"date-time":"2026-04-14T15:48:49Z","timestamp":1776181729555,"version":"3.50.1"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319668444","type":"print"},{"value":"9783319668451","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-66845-1_4","type":"book-chapter","created":{"date-parts":[[2017,8,26]],"date-time":"2017-08-26T11:37:20Z","timestamp":1503747440000},"page":"50-66","source":"Crossref","is-referenced-by-count":71,"title":["Formalising and Monitoring Traffic Rules for Autonomous Vehicles in Isabelle\/HOL"],"prefix":"10.1007","author":[{"given":"Albert","family":"Rizaldi","sequence":"first","affiliation":[]},{"given":"Jonas","family":"Keinholz","sequence":"additional","affiliation":[]},{"given":"Monika","family":"Huber","sequence":"additional","affiliation":[]},{"given":"Jochen","family":"Feldle","sequence":"additional","affiliation":[]},{"given":"Fabian","family":"Immler","sequence":"additional","affiliation":[]},{"given":"Matthias","family":"Althoff","sequence":"additional","affiliation":[]},{"given":"Eric","family":"Hilgendorf","sequence":"additional","affiliation":[]},{"given":"Tobias","family":"Nipkow","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,27]]},"reference":[{"issue":"2","key":"4_CR1","doi-asserted-by":"crossref","first-page":"15:1","DOI":"10.1145\/2699444","volume":"62","author":"DA Basin","year":"2015","unstructured":"Basin, D.A., Klaedtke, F., M\u00fcller, S., Zalinescu, E.: Monitoring metric first-order temporal properties. J. ACM 62(2), 15:1\u201315:45 (2015)","journal-title":"J. ACM"},{"issue":"4","key":"4_CR2","doi-asserted-by":"crossref","first-page":"14:1","DOI":"10.1145\/2000799.2000800","volume":"20","author":"A Bauer","year":"2011","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol. 20(4), 14:1\u201314:64 (2011)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Bender, P., Ziegler, J., Stiller, C.: Lanelets: efficient map representation for autonomous driving. In: Proceedings of the IEEE Intelligent Vehicles Symposium, Michigan, MI, USA, pp. 420\u2013425 (2014)","DOI":"10.1109\/IVS.2014.6856487"},{"key":"4_CR4","unstructured":"Bundesgerichtshof: Sorgfaltspflichten beim \u00fcberholen auf der autobahn, pp. 481\u2013482. Neue Juristische Wochenschrift: NJW (1954)"},{"key":"4_CR5","unstructured":"Burmann, M., He\u00df, R., H\u00fchnermann, K., Jahnke, J., Janker, H.: Stra\u00dfenverkehrsrecht: Kommentar, 24th edn. C.H. Beck (2016)"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Giannakopoulo, D., Havelund, K.: Automata-based verification of temporal properties on running programs. In: Proceedings of the 16th Annual International Conference on Automated Software Engineering (ASE), San Diego, CA, USA, pp. 412\u2013416 (2001)","DOI":"10.1109\/ASE.2001.989841"},{"key":"4_CR7","unstructured":"Gutt, S.: Gesamtes Verkehrsrecht, 1st edn. Nomos (2014)"},{"key":"4_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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). doi: 10.1007\/978-3-642-12251-4_9"},{"key":"4_CR9","unstructured":"Hentschel, P., K\u00f6nig, P., Dauer, P.: Stra\u00dfenverkehrsrecht: Kommentar, 43rd edn. C.H. Beck (2015)"},{"key":"4_CR10","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 (PLMMS 2009), Munich, pp. 38\u201345 (2009)"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Immler, F.: A verified algorithm for geometric zonotope\/hyperplane intersection. In: Proceedings of the International Conference on Certified Programs and Proofs (CPP), Mumbai, India, pp. 129\u2013136 (2015)","DOI":"10.1145\/2676724.2693164"},{"key":"4_CR12","series-title":"Texts in Theoretical Computer Science. EATCS Series","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-50497-0","volume-title":"Decision Procedures - An Algorithmic Point of View","author":"D Kroening","year":"2016","unstructured":"Kroening, D., Strichman, O.: Decision Procedures - An Algorithmic Point of View. Texts in Theoretical Computer Science. EATCS Series, 2nd edn. Springer, Heidelberg (2016)","edition":"2"},{"key":"4_CR13","unstructured":"K\u00fcster, J.C.: Runtime verification on data-carrying traces. Ph.D. thesis, The Australian National University, October 2016"},{"key":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-540-30206-3_12","volume-title":"Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems","author":"O Maler","year":"2004","unstructured":"Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS\/FTRTFT -2004. LNCS, vol. 3253, pp. 152\u2013166. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-30206-3_12"},{"key":"4_CR15","unstructured":"Oberlandesgericht Karlsruhe: Gef\u00e4hrdung des Nachfolgendes beim \u00dcberholen. Neue Zeitschrift f\u00fcr Verkehrsrecht (NZV), pp. 248\u2013249 (1992)"},{"issue":"2","key":"4_CR16","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1016\/S0097-8493(02)00060-2","volume":"26","author":"SC Park","year":"2002","unstructured":"Park, S.C., Shin, H.: Polygonal chain intersection. Comput. Graph. 26(2), 341\u2013350 (2002)","journal-title":"Comput. Graph."},{"key":"4_CR17","doi-asserted-by":"crossref","unstructured":"Rizaldi, A., Althoff, M.: Formalising traffic rules for accountability of autonomous vehicles. In: Proceedings of the 18th IEEE International Conference on Intelligent Transportation Systems, Las Palmas de Gran Canaria Canary Islands, Spain, pp. 1658\u20131665 (2015)","DOI":"10.1109\/ITSC.2015.269"},{"key":"4_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-319-40648-0_14","volume-title":"NASA Formal Methods","author":"A Rizaldi","year":"2016","unstructured":"Rizaldi, A., Immler, F., Althoff, M.: A formally verified checker of the safe distance traffic rules for autonomous vehicles. In: Rayadurgam, S., Tkachuk, O. (eds.) NFM 2016. LNCS, vol. 9690, pp. 175\u2013190. Springer, Cham (2016). doi: 10.1007\/978-3-319-40648-0_14"},{"issue":"5","key":"4_CR19","doi-asserted-by":"crossref","first-page":"370","DOI":"10.1145\/5689.5920","volume":"29","author":"MJ Sergot","year":"1986","unstructured":"Sergot, M.J., Sadri, F., Kowalski, R.A., Kriwaczek, F., Hammond, P., Cory, H.T.: The British Nationality Act as a logic program. Commun. ACM 29(5), 370\u2013386 (1986)","journal-title":"Commun. ACM"},{"key":"4_CR20","doi-asserted-by":"crossref","unstructured":"Werling, M., Ziegler, J., Kammel, S., Thrun, S.: Optimal trajectory generation for dynamic street scenarios in a frenet frame. In: Proceedings of the IEEE International Conference on Robotics and Automation, Anchorage, AK, USA, pp. 987\u2013993 (2010)","DOI":"10.1109\/ROBOT.2010.5509799"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66845-1_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,2]],"date-time":"2019-10-02T16:51:43Z","timestamp":1570035103000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66845-1_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319668444","9783319668451"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66845-1_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}