{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,15]],"date-time":"2025-05-15T23:23:20Z","timestamp":1747351400162,"version":"3.40.3"},"publisher-location":"Cham","reference-count":40,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031606977"},{"type":"electronic","value":"9783031606984"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-60698-4_11","type":"book-chapter","created":{"date-parts":[[2024,5,27]],"date-time":"2024-05-27T00:01:51Z","timestamp":1716768111000},"page":"186-203","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["SMT-Based Aircraft Conflict Detection and\u00a0Resolution"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1792-9858","authenticated-orcid":false,"given":"Saswata","family":"Paul","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3284-1969","authenticated-orcid":false,"given":"Baoluo","family":"Meng","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9543-4968","authenticated-orcid":false,"given":"Christopher","family":"Alexander","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,5,26]]},"reference":[{"issue":"1","key":"11_CR1","doi-asserted-by":"publisher","first-page":"783","DOI":"10.1007\/s10846-013-9948-x","volume":"73","author":"D Alejo","year":"2014","unstructured":"Alejo, D., Cobano, J.A., Heredia, G., Ollero, A.: Collision-free 4D trajectory planning in unmanned aerial vehicles for assembly and structure construction. J. Intell. Robot. Syst. 73(1), 783\u2013795 (2014)","journal-title":"J. Intell. Robot. Syst."},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"Ayhan, S., Costas, P., Samet, H.: Prescriptive analytics system for long-range aircraft conflict detection and resolution. In: Proceedings of the 26th ACM SIGSPATIAL International Conference on Advances in Geographic Information Systems, pp. 239\u2013248 (2018)","DOI":"10.1145\/3274895.3274947"},{"key":"11_CR3","doi-asserted-by":"crossref","unstructured":"Balachandran, S., Manderino, C., Mu\u00f1oz, C., Consiglio, M.: A decentralized framework to support UAS merging and spacing operations in urban canyons. In: 2020 International Conference on Unmanned Aircraft Systems (ICUAS), pp. 204\u2013210. IEEE (2020)","DOI":"10.1109\/ICUAS48674.2020.9213973"},{"key":"11_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154\u2013169. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10722167_15"},{"issue":"2","key":"11_CR5","doi-asserted-by":"publisher","first-page":"15615","DOI":"10.1016\/j.ifacol.2020.12.2496","volume":"53","author":"BK Colbert","year":"2020","unstructured":"Colbert, B.K., Slagel, J.T., Crespo, L.G., Balachandran, S., Munoz, C.: Polysafe: a formally verified algorithm for conflict detection on a polynomial airspace. IFAC-PapersOnLine 53(2), 15615\u201315620 (2020)","journal-title":"IFAC-PapersOnLine"},{"key":"11_CR6","unstructured":"Craven, N., et\u00a0al.: Report: X3 Simulation with National Campaign-Developmental Test (NC-DT) Airspace Partners. Technical report, National Aeronatics and Space Administration (2021). https:\/\/aviationsystems.arc.nasa.gov\/publications\/2021\/NASA-TM-20210011098.pdf. Accessed 25 June 2021"},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"Dowek, G., Munoz, C., Carre\u00f1o, V.: Provably safe coordinated strategy for distributed conflict resolution. In: AIAA Guidance, Navigation, and Control Conference and Exhibit, p.\u00a06047 (2005)","DOI":"10.2514\/6.2005-6047"},{"key":"11_CR9","unstructured":"Dowek, G., Munoz, C., Geser, A.: Tactical conflict detection and resolution in a 3-d airspace. Technical report INSTITUTE FOR COMPUTER APPLICATIONS IN SCIENCE AND ENGINEERING HAMPTON VA (2001)"},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"Durand, N., Alliot, J.M., Noailles, J.: Automatic aircraft conflict resolution using genetic algorithms. In: Proceedings of the 1996 ACM Symposium on Applied Computing, pp. 289\u2013298 (1996)","DOI":"10.1145\/331119.331195"},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-319-63390-9_7","volume-title":"Computer Aided Verification","author":"B Ekici","year":"2017","unstructured":"Ekici, B., et al.: SMTCoq: a plug-in for integrating SMT solvers into Coq. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 126\u2013133. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_7"},{"key":"11_CR12","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":"AL 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. 4576, pp. 177\u2013188. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73445-1_13"},{"key":"11_CR13","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/978-3-642-38574-2_14","volume-title":"Automated Deduction \u2013 CADE-24","author":"S Gao","year":"2013","unstructured":"Gao, S., Kong, S., Clarke, E.M.: dReal: an SMT solver for nonlinear theories over the reals. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 208\u2013214. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_14"},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"Irfan, A., et al.: Towards verification of neural networks for small unmanned aircraft collision avoidance. In: 2020 AIAA\/IEEE 39th Digital Avionics Systems Conference (DASC), pp. 1\u201310. IEEE (2020)","DOI":"10.1109\/DASC50938.2020.9256616"},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"Katz, G., Barrett, C., Tinelli, C., Reynolds, A., Hadarean, L.: Lazy proofs for DPLL (T)-based SMT solvers. In: 2016 Formal Methods in Computer-Aided Design (FMCAD), pp. 93\u2013100. IEEE (2016)","DOI":"10.1109\/FMCAD.2016.7886666"},{"issue":"4","key":"11_CR16","doi-asserted-by":"publisher","first-page":"311","DOI":"10.2514\/atcq.9.4.311","volume":"9","author":"J Krozel","year":"2001","unstructured":"Krozel, J., Peters, M., Bilimoria, K.D., Lee, C., Mitchell, J.S.: System performance characteristics of centralized and decentralized air traffic separation strategies. Air Traffic Control Q. 9(4), 311\u2013332 (2001)","journal-title":"Air Traffic Control Q."},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"Li, M., et al.: Requirements-based automated test generation for safety critical software. In: 2019 IEEE\/AIAA 38th Digital Avionics Systems Conference (DASC), pp. 1\u201310. IEEE (2019)","DOI":"10.1109\/DASC43569.2019.9081726"},{"key":"11_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"646","DOI":"10.1007\/978-3-319-08867-9_43","volume-title":"Computer Aided Verification","author":"T Liang","year":"2014","unstructured":"Liang, T., Reynolds, A., Tinelli, C., Barrett, C., Deters, M.: A DPLL(T) theory solver for a theory of strings and regular expressions. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 646\u2013662. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_43"},{"key":"11_CR19","unstructured":"Meng, B., et\u00a0al.: Towards a correct-by-construction design of integrated modular avionics. In: Conference on Formal Methods in Computer-Aided Design \u2013 FMCAD, p.\u00a0221 (2023)"},{"issue":"1","key":"11_CR20","doi-asserted-by":"publisher","first-page":"18","DOI":"10.3390\/systems9010018","volume":"9","author":"B Meng","year":"2021","unstructured":"Meng, B., et al.: Verdict: a language and framework for engineering cyber resilient and safe system. Systems 9(1), 18 (2021)","journal-title":"Systems"},{"key":"11_CR21","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-319-63046-5_10","volume-title":"Automated Deduction \u2013 CADE 26","author":"B Meng","year":"2017","unstructured":"Meng, B., Reynolds, A., Tinelli, C., Barrett, C.: Relational constraint solving in SMT. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 148\u2013165. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63046-5_10"},{"key":"11_CR22","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1007\/978-3-031-06773-0_40","volume-title":"NASA Formal Methods Symposium","author":"B Meng","year":"2022","unstructured":"Meng, B., Viswanathan, A., Smith, W., Moitra, A., Siu, K., Durling, M.: Synthesis of optimal defenses for system architecture design model in MaXSMT. In: Deshmukh, J.V., Havelund, K., Perez, I. (eds.) NFM 2022. LNCS, vol. 13260, pp. 752\u2013770. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-06773-0_40"},{"key":"11_CR23","doi-asserted-by":"crossref","unstructured":"Munoz, C., Narkawicz, A., Chamberlain, J.: A TCAS-ii resolution advisory detection algorithm. In: AIAA Guidance, Navigation, and Control (GNC) Conference, p.\u00a04622 (2013)","DOI":"10.2514\/6.2013-4622"},{"key":"11_CR24","doi-asserted-by":"crossref","unstructured":"Murrieta-Mendoza, A., Botez, R.M., Patr\u00f3n, R.S.F.: Flight altitude optimization using genetic algorithms considering climb and descent costs in cruise with flight plan information. Technical report SAE Technical Paper (2015)","DOI":"10.4271\/2015-01-2542"},{"key":"11_CR25","doi-asserted-by":"crossref","unstructured":"Narkawicz, A., Mu\u00f1oz, C., Dutle, A.: Sensor uncertainty mitigation and dynamic well clear volumes in DAIDALUS. In: 2018 IEEE\/AIAA 37th Digital Avionics Systems Conference (DASC), pp.\u00a01\u20138. IEEE (2018)","DOI":"10.1109\/DASC.2018.8569468"},{"key":"11_CR26","unstructured":"National Aeronatics and Space Administration: Range and Fuel Consumption Activity. https:\/\/www.grc.nasa.gov\/www\/k-12\/BGP\/Devon\/range_fuel_act.htm. Accessed 18 June 2021"},{"key":"11_CR27","unstructured":"Paul, S.: Emergency Trajectory Generation for Fixed-Wing Aircraft. Master\u2019s thesis, Rensselaer Polytechnic Institute (2018)"},{"key":"11_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-030-76384-8_16","volume-title":"NASA Formal Methods","author":"S Paul","year":"2021","unstructured":"Paul, S., Agha, G.A., Patterson, S., Varela, C.A.: Verification of eventual consensus in synod using a failure-aware actor model. In: Dutle, A., Moscato, M.M., Titolo, L., Mu\u00f1oz, C.A., Perez, I. (eds.) NFM 2021. LNCS, vol. 12673, pp. 249\u2013267. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-76384-8_16"},{"issue":"5","key":"11_CR29","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1109\/MAES.2023.3238378","volume":"38","author":"S Paul","year":"2023","unstructured":"Paul, S., et al.: Formal verification of safety-critical aerospace systems. IEEE Aerosp. Electron. Syst. Mag. 38(5), 72\u201388 (2023). https:\/\/doi.org\/10.1109\/MAES.2023.3238378","journal-title":"IEEE Aerosp. Electron. Syst. Mag."},{"key":"11_CR30","doi-asserted-by":"publisher","unstructured":"Paul, S., Hole, F., Zytek, A., Varela, C.A.: Wind-aware trajectory planning for fixed-wing aircraft in loss of thrust emergencies. In: 2018 IEEE\/AIAA 37th Digital Avionics Systems Conference (DASC), pp. 1\u201310 (2018).https:\/\/doi.org\/10.1109\/DASC.2018.8569842","DOI":"10.1109\/DASC.2018.8569842"},{"key":"11_CR31","doi-asserted-by":"publisher","unstructured":"Paul, S., Patterson, S., Varela, C.A.: Conflict-aware flight planning for avoiding near mid-air collisions. In: The 38th AIAA\/IEEE Digital Avionics Systems Conference (DASC 2019). San Diego, CA (2019).https:\/\/doi.org\/10.1109\/DASC43569.2019.9081658","DOI":"10.1109\/DASC43569.2019.9081658"},{"key":"11_CR32","doi-asserted-by":"crossref","unstructured":"Peters, A., Balachandran, S., Duffy, B., Smalling, K., Consiglio, M., Mu\u00f1oz, C.: Flight test results of a distributed merging algorithm for autonomous UAS operations. In: 2020 AIAA\/IEEE 39th Digital Avionics Systems Conference (DASC), pp.\u00a01\u20137. IEEE (2020)","DOI":"10.1109\/DASC50938.2020.9256619"},{"issue":"1","key":"11_CR33","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1109\/TITS.2017.2693820","volume":"19","author":"AR Pritchett","year":"2017","unstructured":"Pritchett, A.R., Genton, A.: Negotiated decentralized aircraft conflict resolution. IEEE Trans. Intell. Transp. Syst. 19(1), 81\u201391 (2017)","journal-title":"IEEE Trans. Intell. Transp. Syst."},{"key":"11_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/978-3-319-46520-3_16","volume-title":"Automated Technology for Verification and Analysis","author":"A Reynolds","year":"2016","unstructured":"Reynolds, A., Iosif, R., Serban, C., King, T.: A decision procedure for separation logic in SMT. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 244\u2013261. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_16"},{"key":"11_CR35","doi-asserted-by":"crossref","unstructured":"Sacharny, D., Henderson, T.C.: A lane-based approach for large-scale strategic conflict management for UAS service suppliers. In: 2019 International Conference on Unmanned Aircraft Systems (ICUAS), pp. 937\u2013945. IEEE (2019)","DOI":"10.1109\/ICUAS.2019.8798157"},{"key":"11_CR36","doi-asserted-by":"crossref","unstructured":"Shone, R., Glazebrook, K., Zografos, K.G.: Applications of stochastic modeling in air traffic management: methods, challenges and opportunities for solving air traffic problems under uncertainty. Eur. J. Oper. Res. (2020)","DOI":"10.1016\/j.ejor.2020.10.039"},{"key":"11_CR37","doi-asserted-by":"crossref","unstructured":"Siu, K., et\u00a0al.: Architectural and behavioral analysis for cyber security. In: 2019 IEEE\/AIAA 38th Digital Avionics Systems Conference (DASC), pp. 1\u201310. IEEE (2019)","DOI":"10.1109\/DASC43569.2019.9081652"},{"issue":"1","key":"11_CR38","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1109\/TCST.2016.2542046","volume":"25","author":"Y Yang","year":"2016","unstructured":"Yang, Y., Zhang, J., Cai, K.Q., Prandini, M.: Multi-aircraft conflict detection and resolution based on probabilistic reach sets. IEEE Trans. Control Syst. Technol. 25(1), 309\u2013316 (2016)","journal-title":"IEEE Trans. Control Syst. Technol."},{"key":"11_CR39","unstructured":"Young-Brown, F.: FUEL BURN RATES FOR PRIVATE AIRCRAFT (2015). https:\/\/www.sherpareport.com\/aircraft\/fuel-burn-private-aircraft.html. Accessed 18 June 2021"},{"key":"11_CR40","doi-asserted-by":"crossref","unstructured":"Zhang, Y.J., Malikopoulos, A.A., Cassandras, C.G.: Optimal control and coordination of connected and automated vehicles at urban traffic intersections. In: 2016 American Control Conference (ACC), pp. 6227\u20136232. IEEE (2016)","DOI":"10.1109\/ACC.2016.7526648"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-60698-4_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,27]],"date-time":"2024-05-27T00:03:20Z","timestamp":1716768200000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-60698-4_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031606977","9783031606984"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-60698-4_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"26 May 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"NASA Formal Methods Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Moffett Field, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 June 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 June 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}