{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:48:42Z","timestamp":1740098922104,"version":"3.37.3"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319668444"},{"type":"electronic","value":"9783319668451"}],"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_3","type":"book-chapter","created":{"date-parts":[[2017,8,26]],"date-time":"2017-08-26T11:37:20Z","timestamp":1503747440000},"page":"34-49","source":"Crossref","is-referenced-by-count":3,"title":["Spatial Reasoning About Motorway Traffic Safety with Isabelle\/HOL"],"prefix":"10.1007","author":[{"given":"Sven","family":"Linker","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,27]]},"reference":[{"key":"3_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"404","DOI":"10.1007\/978-3-642-24559-6_28","volume-title":"Formal Methods and Software Engineering","author":"M Hilscher","year":"2011","unstructured":"Hilscher, M., Linker, S., Olderog, E.-R., Ravn, A.P.: An abstract model for proving safety of multi-lane traffic manoeuvres. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 404\u2013419. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-24559-6_28"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"Linker, S., Hilscher, M.: proof theory of a multi-lane spatial logic. LMCS 11 (2015)","DOI":"10.2168\/LMCS-11(3:4)2015"},{"key":"3_CR3","unstructured":"Linker, S.: Proofs for traffic safety: combining diagrams and logic. Ph.D. thesis, University of Oldenburg (2015). http:\/\/oops.uni-oldenburg.de\/2337\/"},{"key":"3_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL\u2013A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL\u2013A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)"},{"key":"3_CR5","series-title":"Lecture Notes in Computer Science ( Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-540-71070-7_15","volume-title":"Automated Reasoning","author":"A Platzer","year":"2008","unstructured":"Platzer, A., Quesel, J.-D.: KeYmaera: a hybrid theorem prover for hybrid systems (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 171\u2013178. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-71070-7_15"},{"key":"3_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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). doi: 10.1007\/978-3-642-21437-0_6"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Platzer, A.: The complete proof theory of hybrid systems. In: LICS, pp. 541\u2013550. IEEE (2012)","DOI":"10.1109\/LICS.2012.64"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Rizaldi, A., Althoff, M.: Formalising traffic rules for accountability of autonomous vehicles. In: ITSC, pp. 1658\u20131665. IEEE (2015)","DOI":"10.1109\/ITSC.2015.269"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Kamali, M., Dennis, L.A., McAree, O., Fisher, M., Veres, S.M.: Formal verification of autonomous vehicle platooning. arXiv preprint arXiv:1602.01718 (2016)","DOI":"10.1016\/j.scico.2017.05.006"},{"key":"3_CR10","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. TCS 126, 183\u2013235 (1994)","journal-title":"TCS"},{"key":"3_CR11","first-page":"5","volume":"19","author":"LA Dennis","year":"2012","unstructured":"Dennis, L.A., Fisher, M., Webster, M.P., Bordini, R.H.: Model checking agent programming languages. ASE 19, 5\u201363 (2012)","journal-title":"ASE"},{"key":"3_CR12","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. STTT 1, 134\u2013152 (1997)","journal-title":"STTT"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Campbell, J., Tuncali, C.E., Liu, P., Pavlic, T.P., Ozguner, U., Fainekos, G.: Modeling concurrency and reconfiguration in vehicular systems: a $$\\pi $$ -calculus approach. In: CASE, pp. 523\u2013530 IEEE (2016)","DOI":"10.1109\/COASE.2016.7743450"},{"key":"3_CR14","volume-title":"Principles of Cyber-Physical Systems","author":"R Alur","year":"2015","unstructured":"Alur, R.: Principles of Cyber-Physical Systems. MIT Press, Cambridge (2015)"},{"key":"3_CR15","volume-title":"Hybrid Logic and Its Proof-Theory","author":"T Bra\u00fcner","year":"2010","unstructured":"Bra\u00fcner, T.: Hybrid Logic and Its Proof-Theory. Springer, Netherlands (2010)"},{"key":"3_CR16","doi-asserted-by":"crossref","first-page":"10","DOI":"10.1109\/MC.1985.1662795","volume":"18","author":"BC Moszkowski","year":"1985","unstructured":"Moszkowski, B.C.: A temporal logic for multilevel reasoning about hardware. Computer 18, 10\u201319 (1985)","journal-title":"Computer"},{"key":"3_CR17","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1007\/s11787-012-0052-y","volume":"7","author":"C Benzm\u00fcller","year":"2013","unstructured":"Benzm\u00fcller, C., Paulson, L.: Quantified multimodal logics in simple type theory. Log. Univers. 7, 7\u201320 (2013)","journal-title":"Log. Univers."},{"key":"3_CR18","first-page":"583","volume":"29","author":"GV Bochmann","year":"2017","unstructured":"Bochmann, G.V., Hilscher, M., Linker, S., Olderog, E.R.: Synthesizing and verifying controllers for multi-lane traffic maneuvers. FAC 29, 583\u2013600 (2017)","journal-title":"FAC"},{"key":"3_CR19","series-title":"NASA Monographs in Systems and Software Engineering","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-3-319-48628-4_5","volume-title":"Provably Correct Systems","author":"E-R Olderog","year":"2017","unstructured":"Olderog, E.-R., Ravn, A.P., Wisniewski, R.: Linking discrete and continuous models, applied to traffic manoeuvrers. In: Hinchey, M.G., Bowen, J.P., Olderog, E.-R. (eds.) Provably Correct Systems. NMSSE, pp. 95\u2013120. Springer, Cham (2017). doi: 10.1007\/978-3-319-48628-4_5"},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"H\u00f6lzl, J.: Markov processes in Isabelle\/HOL. In: CPP 2017, pp. 100\u2013111. ACM (2017)","DOI":"10.1145\/3018610.3018628"},{"key":"3_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/978-3-642-39698-4_12","volume-title":"Theories of Programming and Formal Methods","author":"M Hilscher","year":"2013","unstructured":"Hilscher, M., Linker, S., Olderog, E.-R.: Proving safety of traffic manoeuvres on country roads. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) Theories of Programming and Formal Methods. LNCS, vol. 8051, pp. 196\u2013212. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39698-4_12"},{"key":"3_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/978-3-319-46750-4_16","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2016","author":"M Hilscher","year":"2016","unstructured":"Hilscher, M., Schwammberger, M.: An abstract model for proving safety of autonomous urban traffic. In: Sampaio, A., Wang, F. (eds.) ICTAC 2016. LNCS, vol. 9965, pp. 274\u2013292. Springer, Cham (2016). doi: 10.1007\/978-3-319-46750-4_16"},{"key":"3_CR23","doi-asserted-by":"crossref","unstructured":"Xu, B., Li, Q.: A spatial logic for modeling and verification of collision-free control of vehicles. In: ICECCS, pp. 33\u201342. IEEE (2016)","DOI":"10.1109\/ICECCS.2016.014"}],"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_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,2]],"date-time":"2019-10-02T16:51:42Z","timestamp":1570035102000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66845-1_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319668444","9783319668451"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66845-1_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}