{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T16:02:21Z","timestamp":1781193741387,"version":"3.54.1"},"publisher-location":"Cham","reference-count":45,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032280787","type":"print"},{"value":"9783032280794","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"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":[[2026]]},"DOI":"10.1007\/978-3-032-28079-4_25","type":"book-chapter","created":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T15:32:24Z","timestamp":1781191944000},"page":"527-548","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Automatic Certification of\u00a0the\u00a0Active Corner Method for\u00a0Collision Avoidance"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5868-7843","authenticated-orcid":false,"given":"Nishant","family":"Kheterpal","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1362-1976","authenticated-orcid":false,"given":"J. Tanner","family":"Slagel","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2144-1641","authenticated-orcid":false,"given":"Elanor","family":"Tang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-9028-6597","authenticated-orcid":false,"given":"Serra","family":"Dane","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6378-1447","authenticated-orcid":false,"given":"Jean-Baptiste","family":"Jeannin","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,6,12]]},"reference":[{"key":"25_CR1","doi-asserted-by":"crossref","unstructured":"\u00c1brah\u00e1m-Mumm, E., Hannemann, U., Steffen, M.: Verification of hybrid systems: formalization and proof rules in PVS. In: Proceedings of the Seventh IEEE International Conference on Engineering of Complex Computer Systems, pp. 48\u201357. IEEE (2001)","DOI":"10.1109\/ICECCS.2001.930163"},{"issue":"3","key":"25_CR2","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/s10817-009-9149-2","volume":"44","author":"B Akbarpour","year":"2010","unstructured":"Akbarpour, B., Paulson, L.C.: MetiTarski: an automatic theorem prover for real-valued special functions. J. Autom. Reason. 44(3), 175\u2013205 (2010)","journal-title":"J. Autom. Reason."},{"issue":"4","key":"25_CR3","doi-asserted-by":"crossref","first-page":"903","DOI":"10.1109\/TRO.2014.2312453","volume":"30","author":"M Althoff","year":"2014","unstructured":"Althoff, M., Dolan, J.M.: Online verification of automated road vehicles using reachability analysis. IEEE Trans. Rob. 30(4), 903\u2013918 (2014)","journal-title":"IEEE Trans. Rob."},{"key":"25_CR4","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1146\/annurev-control-071420-081941","volume":"4","author":"M Althoff","year":"2021","unstructured":"Althoff, M., Frehse, G., Girard, A.: Set propagation techniques for reachability analysis. Ann. Rev. Control Rob. Auton. Syst. 4, 369\u2013395 (2021)","journal-title":"Ann. Rev. Control Rob. Auton. Syst."},{"key":"25_CR5","doi-asserted-by":"crossref","unstructured":"Ames, A.D., Coogan, S., Egerstedt, M., Notomista, G., Sreenath, K., Tabuada, P.: Control barrier functions: theory and applications. In: 18th European Control Conference (ECC), pp. 3420\u20133431. IEEE (2019)","DOI":"10.23919\/ECC.2019.8796030"},{"key":"25_CR6","doi-asserted-by":"publisher","unstructured":"Armand, M., Faure, G., Gr\u00e9goire, B., Keller, C., Th\u00e9ry, L., Werner, B.: A modular integration of SAT\/SMT solvers to Coq through proof witnesses. In: Jouannaud, JP., Shao, Z. (eds) International Conference on Certified Programs and Proofs, pp. 135\u2013150. Springer, Berlin, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-25379-9_12","DOI":"10.1007\/978-3-642-25379-9_12"},{"key":"25_CR7","unstructured":"Assaf, A., et al.: Dedukti: a logical framework based on the $$\\lambda $$$$\\pi $$-calculus modulo theory (2016)"},{"key":"25_CR8","doi-asserted-by":"crossref","unstructured":"Bansal, S., Chen, M., Herbert, S., Tomlin, C.J.: Hamilton-Jacobi reachability: a brief overview and recent advances. In: IEEE 56th Annual Conference on Decision and Control (CDC), pp. 2242\u20132253. IEEE (2017)","DOI":"10.1109\/CDC.2017.8263977"},{"key":"25_CR9","doi-asserted-by":"publisher","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I. Lecture Notes in Computer Science, vol. 13243, pp. 415\u2013442. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"25_CR10","doi-asserted-by":"publisher","unstructured":"Barbosa, H., et al.: Flexible proof production in an industrial-strength SMT solver. In: 11th International Joint Conference on Automated Reasoning. IJCAR 2022, Haifa, Israel, August 8\u201310, 2022, Proceedings, pp. 15\u201335. Springer-Verlag, Berlin, Heidelberg (2022). https:\/\/doi.org\/10.1007\/978-3-031-10769-6_3","DOI":"10.1007\/978-3-031-10769-6_3"},{"issue":"3","key":"25_CR11","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1023\/A:1015761529444","volume":"28","author":"H Barendregt","year":"2002","unstructured":"Barendregt, H., Barendsen, E.: Autarkic computations in formal proofs. J. Autom. Reason. 28(3), 321\u2013336 (2002)","journal-title":"J. Autom. Reason."},{"key":"25_CR12","doi-asserted-by":"crossref","unstructured":"Becker, H., Zyuzin, N., Monat, R., Darulova, E., Myreen, M.O., Fox, A.: A verified certificate checker for finite-precision error bounds in Coq and HOL4. In: Formal Methods in Computer Aided Design (FMCAD). IEEE (2018)","DOI":"10.23919\/FMCAD.2018.8603019"},{"key":"25_CR13","doi-asserted-by":"publisher","unstructured":"B\u00f6hme, S., Fox, A.C., Sewell, T., Weber, T.: Reconstruction of Z3\u2019s bit-vector proofs in HOL4 and Isabelle\/HOL. In: Jouannaud, JP., Shao, Z. (eds) International Conference on Certified Programs and Proofs, pp. 183\u2013198. Springer, Berlin, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-25379-9_15","DOI":"10.1007\/978-3-642-25379-9_15"},{"key":"25_CR14","doi-asserted-by":"publisher","unstructured":"B\u00f6hme, S., Weber, T.: Fast LCF-style proof reconstruction for Z3. In: Kaufmann, M., Paulson, L.C. (eds) International Conference on Interactive Theorem Proving, pp. 179\u2013194. Springer, Berlin, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14052-5_14","DOI":"10.1007\/978-3-642-14052-5_14"},{"key":"25_CR15","doi-asserted-by":"publisher","unstructured":"Carre\u00f1o, V., Mu\u00f1oz, C.: Aircraft trajectory modeling and alerting algorithm verification. In: Aagaard, M., Harrison, J. (eds) International Conference on Theorem Proving in Higher Order Logics, pp. 90\u2013105. Springer, Berlin, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-44659-1_6","DOI":"10.1007\/3-540-44659-1_6"},{"issue":"2","key":"25_CR16","doi-asserted-by":"crossref","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., Mu\u00f1oz, 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":"25_CR17","doi-asserted-by":"crossref","unstructured":"Colby, C., Lee, P., Necula, G.C., Blau, F., Plesko, M., Cline, K.: A certifying compiler for Java. In: Proceedings of the ACM SIGPLAN 2000 Conference on Programming Language Design and Implementation, pp. 95\u2013107. PLDI \u201900, Association for Computing Machinery, New York, NY, USA (2000)","DOI":"10.1145\/349299.349315"},{"key":"25_CR18","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/3-540-07407-4_17","volume-title":"Automata Theory and Formal Languages","author":"GE Collins","year":"1975","unstructured":"Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Brakhage, H. (ed.) Automata Theory and Formal Languages, pp. 134\u2013183. Springer, Berlin, Heidelberg (1975). https:\/\/doi.org\/10.1007\/3-540-07407-4_17"},{"issue":"1","key":"25_CR19","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1016\/S0747-7171(88)80004-X","volume":"5","author":"JH Davenport","year":"1988","unstructured":"Davenport, J.H., Heintz, J.: Real quantifier elimination is doubly exponential. J. Symb. Comput. 5(1), 29\u201335 (1988)","journal-title":"J. Symb. Comput."},{"key":"25_CR20","doi-asserted-by":"publisher","unstructured":"Foster, S., Huerta\u00a0y Munive, J.J., Gleirscher, M., Struth, G.: Hybrid systems verification with Isabelle\/HOL: simpler syntax, better models, faster proofs. In: Huisman, M., P\u0103s\u0103reanu, C., Zhan, N. (eds) International Symposium on Formal Methods. pp. 367\u2013386. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-90870-6_20","DOI":"10.1007\/978-3-030-90870-6_20"},{"key":"25_CR21","doi-asserted-by":"publisher","unstructured":"Gilbert, F.: Proof certificates in PVS. In: Ayala-Rinc\u00f3n, M., Mu\u00f1oz, C.A. (eds) International Conference on Interactive Theorem Proving, pp. 262\u2013268. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66107-0_17","DOI":"10.1007\/978-3-319-66107-0_17"},{"key":"25_CR22","doi-asserted-by":"publisher","unstructured":"Girard, A.: Reachability of uncertain linear systems using zonotopes. In: Morari, M., Thiele, L. (eds) International Workshop on Hybrid Systems: Computation and Control, pp. 291\u2013305. Springer, Berlin, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31954-2_19","DOI":"10.1007\/978-3-540-31954-2_19"},{"key":"25_CR23","unstructured":"Jouannaud, J.P., Strub, P.Y., Zhang, L.: Certification of SAT solvers in Coq. In: Guangzhou Symposium on Satisfiability in Logic-Based Modeling (2010)"},{"key":"25_CR24","doi-asserted-by":"crossref","unstructured":"Katz, G., Barrett, C., Tinelli, C., Reynolds, A., Hadarean, L.: Lazy proofs for DPLL(T)-based SMT solvers. In: Formal Methods in Computer-Aided Design (FMCAD), pp. 93\u2013100. IEEE (2016)","DOI":"10.1109\/FMCAD.2016.7886666"},{"key":"25_CR25","unstructured":"Kheterpal, N., Tang, E., Jeannin, J.B.: Automating geometric proofs of collision avoidance with active corners. In: Griggio, A., Rungta, N. (eds.) Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design \u2013 FMCAD 2022, vol.\u00a03, pp. 359\u2013368. TU Wien Academic Press (2022)"},{"key":"25_CR26","doi-asserted-by":"crossref","unstructured":"Kousik, S., Holmes, P., Vasudevan, R.: Safe, aggressive quadrotor flight via reachability-based trajectory design. In: Dynamic Systems and Control Conference, vol. 59162, p. V003T19A010. American Society of Mechanical Engineers (2019)","DOI":"10.1115\/DSCC2019-9214"},{"key":"25_CR27","doi-asserted-by":"crossref","unstructured":"Meurer, A., et al.: SymPy: symbolic computing in Python. PeerJ Comput. Sci. 3, e103 (2017)","DOI":"10.7717\/peerj-cs.103"},{"key":"25_CR28","doi-asserted-by":"crossref","unstructured":"Mitsch, S., Ghorbal, K., Platzer, A.: On provably safe obstacle avoidance for autonomous robotic ground vehicles. In: Robotics: Science and Systems IX, Technische Universit\u00e4t Berlin, Berlin, Germany, June 24-June 28, 2013 (2013)","DOI":"10.15607\/RSS.2013.IX.014"},{"key":"25_CR29","doi-asserted-by":"publisher","unstructured":"Moscato, M., Titolo, L., Dutle, A., Munoz, C.A.: Automatic estimation of verified floating-point round-off errors via static analysis. In: Tonetta, S., Schoitsch, E., Bitsch, F. (eds) International Conference on Computer Safety, Reliability, and Security, pp. 213\u2013229. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66266-4_14","DOI":"10.1007\/978-3-319-66266-4_14"},{"key":"25_CR30","doi-asserted-by":"crossref","unstructured":"Mu\u00f1oz, C., et al.: DAIDALUS: detect and avoid alerting logic for unmanned systems. In: 2015 IEEE\/AIAA 34th Digital Avionics Systems Conference (DASC), pp. 5A1\u20131. IEEE (2015)","DOI":"10.1109\/DASC.2015.7311421"},{"key":"25_CR31","unstructured":"Mu\u00f1oz, C.A.: Batch proving and proof scripting in PVS. Tech. rep. (2007)"},{"issue":"3","key":"25_CR32","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1145\/2984450.2984459","volume":"3","author":"CA Mu\u00f1oz","year":"2016","unstructured":"Mu\u00f1oz, C.A., Dutle, A., Narkawicz, A., Upchurch, J.: Unmanned aircraft systems in the national airspace system: a formal methods perspective. ACM SIGLOG News 3(3), 67\u201376 (2016)","journal-title":"ACM SIGLOG News"},{"issue":"4","key":"25_CR33","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1007\/s10817-015-9320-x","volume":"54","author":"A Narkawicz","year":"2015","unstructured":"Narkawicz, A., Mu\u00f1oz, C., Dutle, A.: Formally-verified decision procedures for univariate polynomial computation based on Sturm\u2019s and Tarski\u2019s theorems. J. Autom. Reason. 54(4), 285\u2013326 (2015)","journal-title":"J. Autom. Reason."},{"key":"25_CR34","unstructured":"NASA Formal Methods Team, LaRC and the PVS Community: NASALib: NASA PVS Library of Formal Developments. GitHub repository (2025). https:\/\/github.com\/nasa\/pvslib, version v7.1.1 (stable release)\/current development pre-release"},{"key":"25_CR35","doi-asserted-by":"crossref","unstructured":"Necula, G.C., Lee, P.: The design and implementation of a certifying compiler. In: Proceedings of the ACM SIGPLAN 1998 Conference on Programming Language Design and Implementation, pp. 333\u2013344. PLDI \u201998, Association for Computing Machinery, New York, NY, USA (1998)","DOI":"10.1145\/277650.277752"},{"key":"25_CR36","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle\/HOL: a proof assistant for higher-order logic. Springer, Berlin, Heidelberg (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"25_CR37","unstructured":"N\u00f6tzli, A., et al.: Reconstructing fine-grained proofs of rewrites using a domain-specific language. In: Conference on Formal Methods in Computer-Aided Design (FMCAD 2022), p.\u00a065 (2022)"},{"key":"25_CR38","doi-asserted-by":"publisher","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (eds) International Conference on Automated Deduction, pp. 748\u2013752. Springer, Berlin, Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-55602-8_217","DOI":"10.1007\/3-540-55602-8_217"},{"key":"25_CR39","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-540-71067-7_5","volume-title":"Theorem Proving in Higher Order Logics","author":"S Owre","year":"2008","unstructured":"Owre, S., Shankar, N.: A brief overview of PVS. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) Theorem Proving in Higher Order Logics, pp. 22\u201327. Springer, Berlin, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71067-7_5"},{"key":"25_CR40","doi-asserted-by":"publisher","unstructured":"Prajna, S., Jadbabaie, A.: Safety verification of hybrid systems using barrier certificates. In: Alur, R., Pappas, G.J. (eds) International Workshop on Hybrid Systems: Computation and Control, pp. 477\u2013492. Springer, Berlin, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24743-2_32","DOI":"10.1007\/978-3-540-24743-2_32"},{"key":"25_CR41","unstructured":"RTCA Special Committee 228: DO-365: minimum operational performance standards (MOPS) for detect and avoid (DAA) systems. Tech. rep., RTCA, Inc. (2017). https:\/\/standards.globalspec.com\/std\/14562761\/do-365c\/"},{"key":"25_CR42","doi-asserted-by":"crossref","unstructured":"Schurr, H.J., Fleury, M., Desharnais, M.: Reliable reconstruction of fine-grained proofs in a proof assistant. In: CADE, vol.\u00a028, pp. 450\u2013467 (2021)","DOI":"10.1007\/978-3-030-79876-5_26"},{"key":"25_CR43","unstructured":"Shankar, N., Owre, S., Rushby, J.M., Stringer-Calvert, D.W.: PVS prover guide. Computer Science Laboratory, SRI International, Menlo Park, CA 1, 11\u201312 (2001)"},{"key":"25_CR44","doi-asserted-by":"crossref","unstructured":"Slagel, J.T., White, L., Dutle, A.: Formal verification of semi-algebraic sets and real analytic functions. In: Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 278\u2013290 (2021)","DOI":"10.1145\/3437992.3439933"},{"key":"25_CR45","doi-asserted-by":"publisher","unstructured":"Titolo, L., Feli\u00fa, M.A., Moscato, M., Mu\u00f1oz, C.A.: An abstract interpretation framework for the round-off error analysis of floating-point programs. In: Dillig, I., Palsberg, J. (eds) International Conference on Verification, Model Checking, and Abstract Interpretation, pp. 516\u2013537. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-73721-8_24","DOI":"10.1007\/978-3-319-73721-8_24"}],"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-032-28079-4_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T15:32:34Z","timestamp":1781191954000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-28079-4_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032280787","9783032280794"],"references-count":45,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-28079-4_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"12 June 2026","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":"Los Angeles, 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":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 May 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 May 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/nfm2026.github.io\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}