{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T10:41:04Z","timestamp":1743072064529,"version":"3.40.3"},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319661063"},{"type":"electronic","value":"9783319661070"}],"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-66107-0_22","type":"book-chapter","created":{"date-parts":[[2017,8,20]],"date-time":"2017-08-20T14:13:59Z","timestamp":1503238439000},"page":"336-353","source":"Crossref","is-referenced-by-count":8,"title":["Formally Verified Safe Vertical Maneuvers for Non-deterministic, Accelerating Aircraft\u00a0Dynamics"],"prefix":"10.1007","author":[{"given":"Yanni","family":"Kouskoulas","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Genin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aurora","family":"Schmidt","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean-Baptiste","family":"Jeannin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"22_CR1","unstructured":"Chludzinski, B.J.: Evaluation of TCAS II version 7.1 using the FAA fast-time encounter generator model. Technical report ATC-346, MIT Lincoln Laboratory (2009)"},{"key":"22_CR2","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","year":"2014","unstructured":"Essen, C., Giannakopoulou, D.: Analyzing the next generation airborne collision avoidance system. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 620\u2013635. Springer, Heidelberg (2014). doi:10.1007\/978-3-642-54862-8_54"},{"key":"22_CR3","unstructured":"Federal Aviation Administration: Introduction to TCAS II, Version 7.1 (2011)"},{"key":"22_CR4","first-page":"202","volume":"11","author":"K Ghorbal","year":"2014","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. 11, 202\u2013713 (2014)","journal-title":"J. Aerosp. Inf. Syst."},{"key":"22_CR5","doi-asserted-by":"publisher","first-page":"275","DOI":"10.2514\/atcq.21.3.275","volume":"21","author":"JE Holland","year":"2014","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. 21, 275\u2013297 (2014)","journal-title":"Air Traffic Control Q."},{"key":"22_CR6","doi-asserted-by":"crossref","unstructured":"Jeannin, J., Ghorbal, K., Kouskoulas, Y., Gardner, R., Schmidt, A., Zawadzki, E., Platzer, A.: Formal verification of ACAS X, an industrial airborne collision avoidance system. In: Girault, A., Guan, N. (eds.) 2015 International Conference on Embedded Software, EMSOFT 2015, Amsterdam, The Netherlands, 4\u20139 October 2015. ACM (2015)","DOI":"10.1109\/EMSOFT.2015.7318268"},{"key":"22_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-662-46681-0_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J-B Jeannin","year":"2015","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 2015. LNCS, vol. 9035, pp. 21\u201336. Springer, Heidelberg (2015). doi:10.1007\/978-3-662-46681-0_2"},{"key":"22_CR8","unstructured":"Kochenderfer, M.J., Chryssanthacopoulos, J.P.: Robust airborne collision avoidance through dynamic programming. Technical report ATC-371, MIT Lincoln Laboratory (2010)"},{"issue":"1","key":"22_CR9","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. Lincoln Lab. J. 19(1), 17\u201333 (2012)","journal-title":"Lincoln Lab. J."},{"key":"22_CR10","doi-asserted-by":"crossref","unstructured":"Lee, R., Kochenderfer, M.J., Mengshoel, O.J., Brat, G.P., Owen, M.P.: Adaptive stress testing of airborne collision avoidance systems. In: 2015 IEEE\/AIAA 34th Digital Avionics Systems Conference (DASC), p. 6C2-1. IEEE (2015)","DOI":"10.1109\/DASC.2015.7311613"},{"key":"22_CR11","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":"22_CR12","doi-asserted-by":"crossref","unstructured":"Mu\u00f1oz, C., Narkawicz, A., Chamberlain, J.: A TCAS-II resolution advisory detection algorithm. In: Proceedings of the AIAA Guidance Navigation, and Control Conference and Exhibit 2013, AIAA-2013-4622, Boston, Massachusetts (2013)","DOI":"10.2514\/6.2013-4622"},{"key":"22_CR13","first-page":"209","volume":"17","author":"A Narkawicz","year":"2012","unstructured":"Narkawicz, A., Mu\u00f1oz, C.: Formal verification of conflict detection algorithms for arbitrary trajectories. Reliab. Comput. 17, 209\u2013237 (2012)","journal-title":"Reliab. Comput."},{"key":"22_CR14","doi-asserted-by":"crossref","unstructured":"Narkawicz, A., Mu\u00f1oz, C.: A formally verified conflict detection algorithm for polynomial trajectories. In: Proceedings of the 2015 AIAA Infotech@ Aerospace Conference, Kissimmee, Florida (2015)","DOI":"10.2514\/6.2015-0795"},{"key":"22_CR15","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. 5850, pp. 547\u2013562. Springer, Heidelberg (2009). doi:10.1007\/978-3-642-05089-3_35"},{"issue":"4","key":"22_CR16","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 Trans. Autom. Control 43(4), 509\u2013521 (1998)","journal-title":"IEEE Trans. Autom. Control"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66107-0_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,29]],"date-time":"2022-09-29T06:08:17Z","timestamp":1664431697000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-66107-0_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319661063","9783319661070"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66107-0_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}