{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,2]],"date-time":"2026-01-02T17:29:03Z","timestamp":1767374943694,"version":"3.41.0"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662466803"},{"type":"electronic","value":"9783662466810"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46681-0_2","type":"book-chapter","created":{"date-parts":[[2015,3,30]],"date-time":"2015-03-30T22:56:36Z","timestamp":1427756196000},"page":"21-36","source":"Crossref","is-referenced-by-count":46,"title":["A Formally Verified Hybrid System for the Next-Generation Airborne Collision Avoidance System"],"prefix":"10.1007","author":[{"given":"Jean-Baptiste","family":"Jeannin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Khalil","family":"Ghorbal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yanni","family":"Kouskoulas","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ryan","family":"Gardner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aurora","family":"Schmidt","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Erik","family":"Zawadzki","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andr\u00e9","family":"Platzer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"2_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 (April 2009)"},{"key":"2_CR2","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":"2_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"620","DOI":"10.1007\/978-3-642-54862-8_54","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C. Essen von","year":"2014","unstructured":"von Essen, C., Giannakopoulou, D.: Analyzing the next generation airborne collision avoidance system. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol.\u00a08413, pp. 620\u2013635. Springer, Heidelberg (2014)"},{"key":"2_CR4","unstructured":"Federal Aviation Administration: Introduction to TCAS II, version 7.1 (February 2011)"},{"key":"2_CR5","unstructured":"Federal Aviation Administration TCAS Program Office: Algorithm design description for the surveillance and tracking module of ACAS X, run12 (July 2014)"},{"key":"2_CR6","unstructured":"Federal Aviation Administration TCAS Program Office: Algorithm design description for the threat resolution module of ACAS X, version 3 Rev. 1 (May 2014)"},{"key":"2_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/978-3-540-73445-1_13","volume-title":"Logic, Language, Information and Computation","author":"A.L. Galdino","year":"2007","unstructured":"Galdino, A.L., Mu\u00f1oz, C., Ayala-Rinc\u00f3n, M.: Formal verification of an optimal air traffic conflict resolution and recovery algorithm. In: Leivant, D., de Queiroz, R. (eds.) WoLLIC 2007. LNCS, vol.\u00a04576, pp. 177\u2013188. Springer, Heidelberg (2007)"},{"key":"2_CR8","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. Journal of Aerospace Information Systems (2014)","DOI":"10.2514\/1.I010178"},{"key":"2_CR9","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 Quarterly (2014)","DOI":"10.2514\/atcq.21.3.275"},{"key":"2_CR10","unstructured":"Jeannin, J.B., Ghorbal, K., Kouskoulas, Y., Garnder, R., Schmidt, A., Zawadzki, E., Platzer, A.: A formally verified hybrid system for the next-generation airborne collision avoidance system. Tech. Rep. CMU-CS-14-138, School of Computer Science, Carnegie Mellon University, Pittsburgh, PA (2014), http:\/\/reports-archive.adm.cs.cmu.edu\/anon\/2014\/CMU-CS-14-138.pdf , KeYmaera files available at http:\/\/www.ls.cs.cmu.edu\/pub\/acasx.zip"},{"key":"2_CR11","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 (October 2008)"},{"key":"2_CR12","unstructured":"Kochenderfer, M.J., Chryssanthacopoulos, J.P.: Robust airborne collision avoidance through dynamic programming. Tech. Rep. ATC-371, MIT Lincoln Laboratory (January 2010)"},{"issue":"1","key":"2_CR13","first-page":"17","volume":"19","author":"M.J. Kochenderfer","year":"2012","unstructured":"Kochenderfer, M.J., Holland, J.E., Chryssanthacopoulos, J.P.: Next generation airborne collision avoidance system. Lincoln Laboratory Journal\u00a019(1), 17\u201333 (2012)","journal-title":"Lincoln Laboratory Journal"},{"key":"2_CR14","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":"2_CR15","doi-asserted-by":"crossref","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"},{"key":"2_CR16","doi-asserted-by":"crossref","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"},{"issue":"2","key":"2_CR17","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.\u00a041(2), 143\u2013189 (2008)","journal-title":"J. Autom. Reas."},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"Platzer, A.: Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics. Springer (2010)","DOI":"10.1007\/978-3-642-14509-4"},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"Platzer, A.: Logics of dynamical systems. In: LICS, pp. 13\u201324. IEEE (2012)","DOI":"10.1109\/LICS.2012.13"},{"key":"2_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"547","DOI":"10.1007\/978-3-642-05089-3_35","volume-title":"FM 2009: Formal Methods","author":"A. Platzer","year":"2009","unstructured":"Platzer, A., Clarke, E.M.: Formal verification of curved flight collision avoidance maneuvers: A case study. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol.\u00a05850, pp. 547\u2013562. Springer, Heidelberg (2009)"},{"key":"2_CR21","series-title":"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.\u00a05195, pp. 171\u2013178. Springer, Heidelberg (2008)"},{"issue":"4","key":"2_CR22","doi-asserted-by":"publisher","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 Transactions on Automatic Control\u00a043(4), 509\u2013521 (1998)","journal-title":"IEEE Transactions on Automatic Control"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46681-0_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T19:25:45Z","timestamp":1747855545000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46681-0_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662466803","9783662466810"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46681-0_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}