{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:39:22Z","timestamp":1780994362466,"version":"3.54.1"},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2016,10,4]],"date-time":"2016-10-04T00:00:00Z","timestamp":1475539200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2017,11]]},"DOI":"10.1007\/s10009-016-0434-1","type":"journal-article","created":{"date-parts":[[2016,10,4]],"date-time":"2016-10-04T08:08:18Z","timestamp":1475568498000},"page":"717-741","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":38,"title":["A formally verified hybrid system for safe advisories in the next-generation airborne collision avoidance system"],"prefix":"10.1007","volume":"19","author":[{"given":"Jean-Baptiste","family":"Jeannin","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Khalil","family":"Ghorbal","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yanni","family":"Kouskoulas","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Aurora","family":"Schmidt","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ryan","family":"Gardner","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Stefan","family":"Mitsch","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andr\u00e9","family":"Platzer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2016,10,4]]},"reference":[{"key":"434_CR1","unstructured":"Chludzinski, B.J.: Evaluation of TCAS II version 7.1 using the FAA fast-time encounter generator model. Tech. Rep. ATC-346, MIT Lincoln Laboratory (2009)"},{"key":"434_CR2","doi-asserted-by":"crossref","unstructured":"Collins, G.E.: Hauptvortrag: quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Automata Theory and Formal Languages, LNCS, vol.\u00a033, pp. 134\u2013183. Springer (1975)","DOI":"10.1007\/3-540-07407-4_17"},{"key":"434_CR3","doi-asserted-by":"crossref","unstructured":"Dowek, G., Mu\u00f1oz, C., Carre\u00f1o, V.: Provably safe coordinated strategy for distributed conflict resolution. In: AIAA Guidance Navigation, and Control Conference and Exhibit (2005)","DOI":"10.2514\/6.2005-6047"},{"key":"434_CR4","doi-asserted-by":"publisher","unstructured":"von Essen, C., Giannakopoulou, D.: Analyzing the next generation airborne collision avoidance system. In: TACAS, LNCS, vol. 8413, pp. 620\u2013635. Springer (2014). doi: 10.1007\/978-3-642-54862-8_54","DOI":"10.1007\/978-3-642-54862-8_54"},{"key":"434_CR5","unstructured":"Federal Aviation Administration.: Introduction to TCAS II. Version 7.1 (2011)"},{"key":"434_CR6","unstructured":"Federal Aviation Administration TCAS Program Office.: Algorithm design description for the surveillance and tracking module of ACAS X. Run12 (2014)"},{"key":"434_CR7","unstructured":"Federal Aviation Administration TCAS Program Office.: Algorithm design description for the threat resolution module of ACAS X. Version 3 Rev. 1 (2014)"},{"key":"434_CR8","doi-asserted-by":"crossref","unstructured":"Felty, A., Middeldorp, A. (eds.): International Conference on Automated Deduction, CADE\u201915, Berlin, Germany, Proceedings, LNCS, vol. 9195. Springer (2015)","DOI":"10.1007\/978-3-319-21401-6"},{"key":"434_CR9","doi-asserted-by":"publisher","unstructured":"Fulton, N., Mitsch, S., Quesel, J.D., V\u00f6lp, M., Platzer, A.: KeYmaera X: an axiomatic tactical theorem prover for hybrid systems. In: Felty and Middeldorp [8], pp. 527\u2013538. doi: 10.1007\/978-3-319-21401-6_36","DOI":"10.1007\/978-3-319-21401-6_36"},{"key":"434_CR10","doi-asserted-by":"crossref","unstructured":"Galdino, A., Mu\u00f1oz, C., Ayala, M.: Formal verification of an optimal air traffic conflict resolution and recovery algorithm. In: WoLLIC, LNCS, vol. 4576. Springer (2007)","DOI":"10.1007\/978-3-540-73445-1_13"},{"key":"434_CR11","doi-asserted-by":"crossref","unstructured":"Ghorbal, K., Jeannin, J.B., Zawadzki, E., Platzer, A., Gordon, G.J., Capell, P.: Hybrid theorem proving of aerospace systems: applications and challenges. J. Aerosp. Inf. Syst. (2014)","DOI":"10.2514\/1.I010178"},{"key":"434_CR12","doi-asserted-by":"crossref","unstructured":"Holland, J.E., Kochenderfer, M.J., Olson, W.A.: Optimizing the next generation collision avoidance system for safe, suitable, and acceptable operational performance. Air Traffic Control Q. (2014)","DOI":"10.2514\/atcq.21.3.275"},{"key":"434_CR13","doi-asserted-by":"publisher","unstructured":"Jeannin, J.B., Ghorbal, K., Kouskoulas, Y., Gardner, R., Schmidt, A., Zawadzki, E., Platzer, A.: A formally verified hybrid system for the next-generation airborne collision avoidance system. In: Baier, C., Tinelli, C. (eds.) TACAS, LNCS, vol. 9035, pp. 21\u201336. Springer (2015). doi: 10.1007\/978-3-662-46680-3_2","DOI":"10.1007\/978-3-662-46680-3_2"},{"key":"434_CR14","unstructured":"Kochenderfer, M.J., Chryssanthacopoulos, J.P.: Robust airborne collision avoidance through dynamic programming. Tech. Rep. ATC-371, MIT Lincoln Laboratory (2010)"},{"key":"434_CR15","unstructured":"Kochenderfer, M.J., Espindle, L.P., Kuchar, J.K., Griffith, J.D.: Correlated encounter model for cooperative aircraft in the national airspace system version 1.0. Tech. Rep. ATC-344, MIT Lincoln Laboratory (2008)"},{"issue":"1","key":"434_CR16","first-page":"17","volume":"19","author":"MJ Kochenderfer","year":"2012","unstructured":"Kochenderfer, M.J., Holland, J.E., Chryssanthacopoulos, J.P.: Next generation airborne collision avoidance system. Linc. Lab. J. 19(1), 17\u201333 (2012)","journal-title":"Linc. Lab. J."},{"key":"434_CR17","doi-asserted-by":"crossref","unstructured":"Kochenderfer, M.J., Monath, N.: Compression of optimal value functions for Markov decision processes. In: Data Compression Conference. Snowbird, Utah (2013)","DOI":"10.1109\/DCC.2013.81"},{"key":"434_CR18","doi-asserted-by":"publisher","unstructured":"Loos, S.M., Renshaw, D.W., Platzer, A.: Formal verification of distributed aircraft controllers. In: HSCC, pp. 125\u2013130. ACM (2013). doi: 10.1145\/2461328.2461350","DOI":"10.1145\/2461328.2461350"},{"key":"434_CR19","doi-asserted-by":"publisher","unstructured":"Lygeros, J., Lynch, N.: On the formal verification of the TCAS conflict resolution algorithms. In: IEEE Decision and Control, vol.\u00a02, pp. 1829\u20131834. IEEE (1997). doi: 10.1109\/CDC.1997.657846","DOI":"10.1109\/CDC.1997.657846"},{"issue":"2","key":"434_CR20","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/s10817-008-9103-8","volume":"41","author":"A Platzer","year":"2008","unstructured":"Platzer, A.: Differential dynamic logic for hybrid systems. J. Autom. Reas. 41(2), 143\u2013189 (2008). doi: 10.1007\/s10817-008-9103-8","journal-title":"J. Autom. Reas."},{"key":"434_CR21","doi-asserted-by":"publisher","unstructured":"Platzer, A.: Logical analysis of hybrid systems: Proving theorems for complex dynamics. Springer (2010). doi: 10.1007\/978-3-642-14509-4","DOI":"10.1007\/978-3-642-14509-4"},{"key":"434_CR22","doi-asserted-by":"publisher","unstructured":"Platzer, A.: Logics of dynamical systems. In: LICS, pp. 13\u201324. IEEE (2012). doi: 10.1109\/LICS.2012.13","DOI":"10.1109\/LICS.2012.13"},{"key":"434_CR23","doi-asserted-by":"publisher","unstructured":"Platzer, A.: A uniform substitution calculus for differential dynamic logic. In: Felty and Middeldorp [8], pp. 467\u2013481. doi: 10.1007\/978-3-319-21401-6_32","DOI":"10.1007\/978-3-319-21401-6_32"},{"key":"434_CR24","doi-asserted-by":"publisher","unstructured":"Platzer, A., Clarke, E.M.: Formal verification of curved flight collision avoidance maneuvers: A case study. In: FM, LNCS, vol. 5850, pp. 547\u2013562. Springer (2009). doi: 10.1007\/978-3-642-05089-3_35","DOI":"10.1007\/978-3-642-05089-3_35"},{"issue":"4","key":"434_CR25","doi-asserted-by":"crossref","first-page":"509","DOI":"10.1109\/9.664154","volume":"43","author":"C Tomlin","year":"1998","unstructured":"Tomlin, C., Pappas, G.J., Sastry, S.: Conflict resolution for air traffic management: A study in multiagent hybrid systems. IEEE Trans. Autom. Control 43(4), 509\u2013521 (1998)","journal-title":"IEEE Trans. Autom. Control"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-016-0434-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-016-0434-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-016-0434-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,14]],"date-time":"2019-09-14T03:09:03Z","timestamp":1568430543000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-016-0434-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,10,4]]},"references-count":25,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2017,11]]}},"alternative-id":["434"],"URL":"https:\/\/doi.org\/10.1007\/s10009-016-0434-1","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,10,4]]}}}