{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T16:11:05Z","timestamp":1746115865419,"version":"3.40.4"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642412011"},{"type":"electronic","value":"9783642412028"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-41202-8_7","type":"book-chapter","created":{"date-parts":[[2013,10,21]],"date-time":"2013-10-21T05:11:19Z","timestamp":1382332279000},"page":"86-101","source":"Crossref","is-referenced-by-count":0,"title":["Verifying an Aircraft Proximity Characterization Method in Coq"],"prefix":"10.1007","author":[{"given":"Dongxi","family":"Liu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Neale L.","family":"Fulton","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John","family":"Zic","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"de Groot","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"7_CR1","unstructured":"Fulton, N.L., Huynh, U.: A survey of aircraft proximity applications based on the Apollonius intercept. Report EP103115, CMIS, CSIRO, Canberra, ACT 2601, Australia (2010)"},{"issue":"5","key":"7_CR2","doi-asserted-by":"crossref","first-page":"2787","DOI":"10.1109\/TSMCA.2010.2093890","volume":"41","author":"J. Ellerbroek","year":"2011","unstructured":"Ellerbroek, J., Visser, M., van Dam, S.B.J., Mulder, M., van Paassen, M.M.R.: Design of an airborne three-dimensional, separation assistance display. IEEE Trans. Systems, Man, and Cybernetics - Part A: Systems and Humans\u00a041(5), 2787\u20132794 (2011)","journal-title":"IEEE Trans. Systems, Man, and Cybernetics - Part A: Systems and Humans"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"Robb, M., White, B., Tsourdos, A.: Earliest intercept line guidance: a novel concept for improving mid-course guidance in area air defence. In: AIAA Guidance, Navigation, and Control Conference and Exhibit, San Francisco, California (August 2005)","DOI":"10.2514\/6.2005-5971"},{"issue":"3","key":"7_CR4","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1007\/s10009-002-0084-3","volume":"4","author":"C. Mu\u00f1oz","year":"2003","unstructured":"Mu\u00f1oz, C., Carre\u00f1o, V., Dowek, G., Butler, R.W.: Formal verification of conflict detection algorithms. International Journal on Software Tools for Technology Transfer\u00a04(3), 371\u2013380 (2003)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"7_CR5","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, San Francisco, California (August 2005)","DOI":"10.2514\/6.2005-6047"},{"key":"7_CR6","unstructured":"Dowek, G., Mu\u00f1oz, C.: Conflict detection and resolution for 1,2,. . . ,n aircraft. In: 7th AIAA Aviation Technology, Integration and Operations Conference, Belfast, Northern Ireland (September 2007)"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/11813040_5","volume-title":"FM 2006: Formal Methods","author":"S. Umeno","year":"2006","unstructured":"Umeno, S., Lynch, N.: Proving safety properties of an aircraft landing protocol using I\/O automata and the PVS theorem prover: A case study. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol.\u00a04085, pp. 64\u201380. Springer, Heidelberg (2006)"},{"key":"7_CR8","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":"7_CR9","unstructured":"The Coq Deleopment Team: The Coq Proof Assistant, http:\/\/coq.inria.fr (accessed May 30, 2012)"},{"key":"7_CR10","unstructured":"Liu, D., Fulton, N.L., Zic, J., de Groot, M.: Formalization of aircraft proximity characterization in coq. Report EP125569, ICT Centre and CMIS, CSIRO, Marsfield, NSW 2122, Australia (2012)"},{"issue":"4","key":"7_CR11","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1016\/j.jal.2005.10.008","volume":"4","author":"J.H. Siekmann","year":"2006","unstructured":"Siekmann, J.H., Benzm\u00fcller, C., Autexier, S.: Computer supported mathematics with omegamega. J. Applied Logic\u00a04(4), 533\u2013559 (2006)","journal-title":"J. Applied Logic"},{"key":"7_CR12","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1145\/1007512.1007536","volume-title":"Proceedings of the 2004 ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2004","author":"C.A. Mu\u00f1oz","year":"2004","unstructured":"Mu\u00f1oz, C.A., Dowek, G., Carre\u00f1o, V.: Modeling and verification of an air traffic concept of operations. In: Proceedings of the 2004 ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2004, pp. 175\u2013182. ACM, New York (2004)"},{"key":"7_CR13","unstructured":"Goodloe, A., Mu\u00f1oz, C.: Compositional verification of a communication protocol for a remotely operated aircraft. Science of Computer Programming (2011) (in press)"},{"issue":"4","key":"7_CR14","doi-asserted-by":"publisher","first-page":"489","DOI":"10.1007\/s10817-010-9209-7","volume":"48","author":"P. Janicic","year":"2012","unstructured":"Janicic, P., Narboux, J., Quaresma, P.: The area method - a recapitulation. J. Autom. Reasoning\u00a048(4), 489\u2013532 (2012)","journal-title":"J. Autom. Reasoning"},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/978-3-642-21898-9_32","volume-title":"Computational Science and Its Applications - ICCSA 2011","author":"T.-M. Pham","year":"2011","unstructured":"Pham, T.-M., Bertot, Y., Narboux, J.: A Coq-based library for interactive and automated theorem proving in plane geometry. In: Murgante, B., Gervasi, O., Iglesias, A., Taniar, D., Apduhan, B.O. (eds.) ICCSA 2011, Part IV. LNCS, vol.\u00a06785, pp. 368\u2013383. Springer, Heidelberg (2011)"},{"key":"7_CR16","series-title":"Lecture Notes in Computer Science","volume-title":"Theorem Proving in Higher Order Logics","year":"2004","unstructured":"Slind, K., Bunker, A., Gopalakrishnan, G. (eds.): TPHOLs 2004. LNCS, vol.\u00a03223. Springer, Heidelberg (2004)"},{"key":"7_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-642-25379-9_8","volume-title":"Certified Programs and Proofs","author":"J.D. G\u00e9nevaux","year":"2011","unstructured":"G\u00e9nevaux, J.D., Narboux, J., Schreck, P.: Formalization of Wu\u2019s simple method in Coq. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol.\u00a07086, pp. 71\u201386. Springer, Heidelberg (2011)"},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"Chou, S.C., Gao, X.S., Zhang, J.Z.: Automated production of traditional proofs for constructive geometry theorems. In: Proceedings of Eighth Annual IEEE Symposium on Logic in Computer Science, pp. 48\u201356 (June 1993)","DOI":"10.1109\/LICS.1993.287601"},{"issue":"2","key":"7_CR19","first-page":"159","volume":"21","author":"W.T. Wu","year":"1978","unstructured":"Wu, W.T.: On the decision problem and the mechanization of theorem proving in elementary geometry. Scientia Sinica\u00a021(2), 159\u2013172 (1978)","journal-title":"Scientia Sinica"},{"key":"7_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/3-540-39185-1_7","volume-title":"Types for Proofs and Programs","author":"L. Cruz-Filipe","year":"2003","unstructured":"Cruz-Filipe, L.: A constructive formalization of the fundamental theorem of calculus. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol.\u00a02646, pp. 108\u2013126. Springer, Heidelberg (2003)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-41202-8_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T17:42:46Z","timestamp":1746034966000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-41202-8_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642412011","9783642412028"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-41202-8_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}