{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T05:40:24Z","timestamp":1737006024450,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540425410"},{"type":"electronic","value":"9783540447986"}],"license":[{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44798-9_31","type":"book-chapter","created":{"date-parts":[[2007,5,3]],"date-time":"2007-05-03T17:16:15Z","timestamp":1178212575000},"page":"403-417","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Formal Verification of Conflict Detection Algorithms"],"prefix":"10.1007","author":[{"given":"Ricky","family":"Butler","sequence":"first","affiliation":[]},{"given":"V\u00edctor","family":"Carre\u00f1o","sequence":"additional","affiliation":[]},{"given":"Gilles","family":"Dowek","sequence":"additional","affiliation":[]},{"given":"C\u00e9sar","family":"Mu\u00f1oz","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,8,24]]},"reference":[{"key":"31_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1007\/BFb0105402","volume-title":"Ninth international Conference on Theorem Proving in Higher Order Logics TPHOL","author":"B. Dutertre","year":"1996","unstructured":"B. Dutertre. Elements of mathematical analysis in PVS. In J. Von Wright, J. Grundy, and J. Harrison, editors, Ninth international Conference on Theorem Proving in Higher Order Logics TPHOL, volume 1125 of Lecture Notes in Computer Science, pages 141\u2013156, Turku, Finland, August 1996. Springer Verlag."},{"key":"31_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1007\/3-540-44659-1_6","volume-title":"Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000","author":"V. Carre\u00f1o","year":"2000","unstructured":"V. Carre\u00f1o and C. Mu\u00f1oz. Aircraft trajectory modeling and alerting algorithm verification. In J. Harrison and M. Aagaard, editors, Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000, volume 1869 of Lecture Notes in Computer Science, pages 90\u2013105. Springer-Verlag, 2000. An earlier version appears as report NASA\/CR-2000-210097 ICASE No. 2000-16."},{"key":"31_CR3","volume-title":"Technical Report NASA\/CR-2001-210853 ICASE Report No. 2001-7","author":"G. Dowek","year":"2001","unstructured":"G. Dowek, C. Mu\u00f1oz, and A. Geser. Tactical conflict detection and resolution in a 3-D airspace. Technical Report NASA\/CR-2001-210853 ICASE Report No. 2001-7, ICASE-NASA Langley, ICASE Mail Stop 132C, NASA Langley Research Center, Hampton VA 23681-2199, USA, April 2001."},{"unstructured":"J. Kuchar and Jr. R. Hansman. A unified methodology for the evaluation of hazard alerting systems. Technical Report ASL-95-1, ASL MIT Aeronautical System Laboratory, January 1995.","key":"31_CR4"},{"doi-asserted-by":"crossref","unstructured":"J. Kuchar and L. Yang. Survey of conflict detection and resolution modeling methods. In AIAA Guidance, Navigation, and Control Conference, volume AIAA-97-3732, pages 1388\u20131397, New Orleans, LA, August 1997.","key":"31_CR5","DOI":"10.2514\/6.1997-3732"},{"doi-asserted-by":"crossref","unstructured":"J. Lygeros and N. Lynch. On the formal verification of the TCAS conflict resolution algorithms. In Proceedings 36th IEEE Conference on Decision and Control, San Diego, CA, pages 1829\u20131834, December 1997. Extended abstract.","key":"31_CR6","DOI":"10.1109\/CDC.1997.657846"},{"key":"31_CR7","volume-title":"Technical Report NASA\/TM-2001-210864","author":"C. Mu\u00f1oz","year":"2001","unstructured":"C. Mu\u00f1oz, R.W. Butler, V. Carre\u00f1o, and G. Dowek. On the verification of conflict detection algorithms. Technical Report NASA\/TM-2001-210864, NASA Langley Research Center, NASA LaRC Hampton VA 23681-2199, USA, May 2001."},{"doi-asserted-by":"crossref","unstructured":"S. Owre, J. M. Rushby, and N. Shankar. PVS: A prototype verification system. In Deepak Kapur, editor, 11th International Conference on Automated Deduction (CADE), volume 607 of Lecture Notes in Artificial Intelligence, pages 748\u2013752, Saratoga, NY, June 1992. Springer-Verlag.","key":"31_CR8","DOI":"10.1007\/3-540-55602-8_217"},{"unstructured":"Radio Technical Commission for Aeronautics. Final report of the RTCA board of directors\u2019 select committee on free flight. Technical Report Issued 1-18-95, RTCA, Washington, DC, 1995.","key":"31_CR9"},{"unstructured":"L. Rine, T. Abbott, G. Lohr, D. Elliott, M. Waller, and R. Perry. The flight deck perspective of the NASA Langley AILS concept. Technical Report NASA\/TM-2000-209841, NASA, January 2000.","key":"31_CR10"},{"doi-asserted-by":"crossref","unstructured":"C. Tomlin, G. Pappas, and S. Sastry. Conflict resolution for air traffic management: A study in multi-agent hybrid systems. IEEE Transactions on Automatic Control, 43(4), April 1998.","key":"31_CR11","DOI":"10.1109\/9.664154"}],"container-title":["Lecture Notes in Computer Science","Correct Hardware Design and Verification Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44798-9_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T00:57:29Z","timestamp":1736989049000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44798-9_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540425410","9783540447986"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/3-540-44798-9_31","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]},"assertion":[{"value":"24 August 2001","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}