{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:37:07Z","timestamp":1742913427185,"version":"3.40.3"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030955601"},{"type":"electronic","value":"9783030955618"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-030-95561-8_9","type":"book-chapter","created":{"date-parts":[[2022,2,21]],"date-time":"2022-02-21T19:04:21Z","timestamp":1645470261000},"page":"147-164","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Formal Verification of\u00a0Neural Network Controllers for\u00a0Collision-Free Flight"],"prefix":"10.1007","author":[{"given":"Daniel","family":"Genin","sequence":"first","affiliation":[]},{"given":"Ivan","family":"Papusha","sequence":"additional","affiliation":[]},{"given":"Joshua","family":"Brul\u00e9","sequence":"additional","affiliation":[]},{"given":"Tyler","family":"Young","sequence":"additional","affiliation":[]},{"given":"Galen","family":"Mullins","sequence":"additional","affiliation":[]},{"given":"Yanni","family":"Kouskoulas","sequence":"additional","affiliation":[]},{"given":"Rosa","family":"Wu","sequence":"additional","affiliation":[]},{"given":"Aurora","family":"Schmidt","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,2,22]]},"reference":[{"key":"9_CR1","unstructured":"Amodei, D., Olah, C., Steinhardt, J., Christiano, P., Schulman, J., Man\u00e9, D.: Concrete problems in AI safety, July 2016. arXiv:1606.06565 [cs.AI]"},{"key":"9_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/978-3-030-53288-8_4","volume-title":"Computer Aided Verification","author":"S Bak","year":"2020","unstructured":"Bak, S., Tran, H.-D., Hobbs, K., Johnson, T.T.: Improved geometric path enumeration for verifying ReLU neural networks. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 66\u201396. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_4"},{"key":"9_CR3","unstructured":"National Transportation Safety Board: Preliminary report released for crash involving pedestrian, Uber Technologies Inc, test vehicle (2018). https:\/\/www.ntsb.gov\/news\/press-releases\/Pages\/NR20180524.aspx. Accessed 23 Sept 2020"},{"issue":"1","key":"9_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1186\/s42400-019-0027-x","volume":"2","author":"T Chen","year":"2019","unstructured":"Chen, T., Liu, J., Xiang, Y., Niu, W., Tong, E., Han, Z.: Adversarial attack and defense in reinforcement learning-from AI security view. Cybersecurity 2(1), 1\u201322 (2019). https:\/\/doi.org\/10.1186\/s42400-019-0027-x","journal-title":"Cybersecurity"},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"Dutta, S., Chen, X., Jha, S., Sankaranarayanan, S., Tiwari, A.: Sherlock - a tool for verification of neural network feedback systems. In: ACM International Conference on Hybrid Systems: Computation and Control (HSCC), pp. 262\u2013263. Association for Computing Machinery, New York (2019)","DOI":"10.1145\/3302504.3313351"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"Gehr, T., Mirman, M., Drachsler-Cohen, D., Tsankov, P., Chaudhuri, S., Vechev, M.: AI$$^2$$: safety and robustness certification of neural networks with abstract interpretation. In: IEEE Symposium on Security and Privacy (SP), pp. 3\u201318 (2018)","DOI":"10.1109\/SP.2018.00058"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"Huang, C., Fan, J., Li, W., Chen, X., Zhu, Q.: ReachNN: reachability analysis of neural-network controlled systems. ACM Trans. Embed. Comput. Syst. 18(5s) (2019)","DOI":"10.1145\/3358228"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-63387-9_1","volume-title":"Computer Aided Verification","author":"X Huang","year":"2017","unstructured":"Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety verification of deep neural networks. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 3\u201329. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_1"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"Ivanov, R., Weimer, J., Alur, R., Pappas, G.J., Lee, I.: Verisig: verifying safety properties of hybrid systems with neural network controllers. In: ACM International Conference on Hybrid Systems: Computation and Control (HSCC), pp. 169\u2013178 (2019)","DOI":"10.1145\/3302504.3311806"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Jeannin, J., et al.: Formal verification of ACAS X, an industrial airborne collision avoidance system. In: Girault, A., Guan, N. (eds.) International Conference on Embedded Software, EMSOFT 2015, Amsterdam, The Netherlands, 4\u20139 October 2015. ACM (2015)","DOI":"10.1109\/EMSOFT.2015.7318268"},{"key":"9_CR11","unstructured":"Johnson, T.T., et al.: ARCH-COMP20 category report: artificial intelligence and neural network control systems (AINNCS) for continuous and hybrid systems plants. In: Frehse, G., Althoff, M. (eds.) International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH20). EPiC Series in Computing, vol. 74, pp. 107\u2013139 (2020)"},{"issue":"6","key":"9_CR12","doi-asserted-by":"publisher","first-page":"1132","DOI":"10.2514\/1.G005233","volume":"44","author":"KD Julian","year":"2021","unstructured":"Julian, K.D., Kochenderfer, M.J.: Reachability analysis for neural network aircraft collision avoidance systems. J. Guid. Control. Dyn. 44(6), 1132\u20131142 (2021)","journal-title":"J. Guid. Control. Dyn."},{"key":"9_CR13","unstructured":"Julian, K.D., Sharma, S., Jeannin, J.B., Kochenderfer, M.J.: Verifying aircraft collision avoidance neural networks through linear approximations of safe regions. In: AIAA Spring Symposium (2019). arXiv:1903.00762 [cs.SY]"},{"key":"9_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-319-63387-9_5","volume-title":"Computer Aided Verification","author":"G Katz","year":"2017","unstructured":"Katz, G., Barrett, C., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: an efficient SMT solver for verifying deep neural networks. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 97\u2013117. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_5"},{"key":"9_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/978-3-030-25540-4_26","volume-title":"Computer Aided Verification","author":"G Katz","year":"2019","unstructured":"Katz, G., et al.: The marabou framework for verification and analysis of deep neural networks. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 443\u2013452. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_26"},{"issue":"1","key":"9_CR16","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":"9_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1007\/978-3-319-66107-0_22","volume-title":"Interactive Theorem Proving","author":"Y Kouskoulas","year":"2017","unstructured":"Kouskoulas, Y., Genin, D., Schmidt, A., Jeannin, J.-B.: Formally verified safe vertical maneuvers for non-deterministic, accelerating aircraft dynamics. In: Ayala-Rinc\u00f3n, M., Mu\u00f1oz, C.A. (eds.) ITP 2017. LNCS, vol. 10499, pp. 336\u2013353. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66107-0_22"},{"key":"9_CR18","doi-asserted-by":"crossref","unstructured":"Kouskoulas, Y., Schmidt, A., Jeannin, J.B., Genin, D., Lopez, J.: Provably safe controller synthesis using safety proofs as building blocks. In: 7th International Conference in Software Engineering Research and Innovation (CONISOFT), pp. 26\u201335 (2019)","DOI":"10.1109\/CONISOFT.2019.00015"},{"key":"9_CR19","unstructured":"Liu, C., Arnon, T., Lazarus, C., Barrett, C., Kochenderfer, M.J.: Algorithms for verifying deep neural networks (2019)"},{"key":"9_CR20","unstructured":"Lopez, D.M., Johnson, T., Tran, H.D., Bak, S., Chen, X., Hobbs, K.L.: Formal methods for intelligent aerospace systems. In: Verification of Neural Network Compression of ACAS Xu Lookup Tables with Star Set Reachability. AIAA SciTech Forum (2021)"},{"key":"9_CR21","doi-asserted-by":"crossref","unstructured":"McCloskey, M., Cohen, N.J.: Catastrophic interference in connectionist networks: the sequential learning problem. In: Psychology of Learning and Motivation, vol. 24, pp. 109\u2013165. Elsevier (1989)","DOI":"10.1016\/S0079-7421(08)60536-8"},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"Mitsch, S., Platzer, A.: ModelPlex: verified runtime validation of verified cyber-physical system models. Formal Methods Syst. Des. 49(1), 33\u201374 (2016). Special issue of selected papers from RV 2014","DOI":"10.1007\/s10703-016-0241-z"},{"key":"9_CR23","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":"9_CR24","unstructured":"Papusha, I., Topcu, U., Carr, S., Lauffer, N.: Affine multiplexing networks: system analysis, learning, and computation, April 2018. arXiv:1805.00164 [math.OC]"},{"key":"9_CR25","unstructured":"Papusha, I., Wu, R., Brul\u00e9, J., Kouskoulas, Y., Genin, D., Schmidt, A.: Incorrect by construction: fine tuning neural networks for guaranteed performance on finite sets of examples. In: 3rd Workshop on Formal Methods for ML-Enabled Autonomous Systems (FoMLAS), July 2020. arXiv:2008.01204 [cs.LG]"},{"key":"9_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/978-3-030-30281-8_2","volume-title":"Quantitative Evaluation of Systems","author":"A Platzer","year":"2019","unstructured":"Platzer, A.: The logical path to autonomous cyber-physical systems. In: Parker, D., Wolf, V. (eds.) QEST 2019. LNCS, vol. 11785, pp. 25\u201333. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30281-8_2"},{"key":"9_CR27","unstructured":"Wolfram Research Inc: Mathematica, Version 12.1, Champaign, IL (2020). https:\/\/www.wolfram.com\/mathematica"}],"container-title":["Lecture Notes in Computer Science","Software Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-95561-8_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,2,21]],"date-time":"2022-02-21T19:04:59Z","timestamp":1645470299000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-95561-8_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030955601","9783030955618"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-95561-8_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"22 February 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NSV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Workshop on Numerical Software Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nsv2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/nsv2021.github.io\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"100% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3,7","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"1","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}