{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T04:25:21Z","timestamp":1743049521514,"version":"3.40.3"},"publisher-location":"Cham","reference-count":67,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031711619"},{"type":"electronic","value":"9783031711626"}],"license":[{"start":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T00:00:00Z","timestamp":1726012800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T00:00:00Z","timestamp":1726012800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Autonomous systems are increasingly implemented using end-to-end learning-based controllers. Such controllers make decisions that are executed on the real system, with images as one of the primary sensing modalities. Deep neural networks form a fundamental building block of such controllers. Unfortunately, the existing neural-network verification tools do not scale to inputs with thousands of dimensions\u2014especially when the individual inputs (such as pixels) are devoid of clear physical meaning. This paper takes a step towards connecting exhaustive closed-loop verification with high-dimensional controllers. Our key insight is that the behavior of a high-dimensional vision-based controller can be approximated with several low-dimensional controllers. To balance the approximation accuracy and verifiability of our low-dimensional controllers, we leverage the latest verification-aware knowledge distillation. Then, we inflate low-dimensional reachability results with statistical approximation errors, yielding a high-confidence reachability guarantee for the high-dimensional controller. We investigate two inflation techniques\u2014based on trajectories and control actions\u2014both of which show convincing performance in three OpenAI gym benchmarks.<\/jats:p>","DOI":"10.1007\/978-3-031-71162-6_20","type":"book-chapter","created":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T02:02:27Z","timestamp":1725933747000},"page":"381-402","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Bridging Dimensions: Confident Reachability for\u00a0High-Dimensional Controllers"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2265-7586","authenticated-orcid":false,"given":"Yuang","family":"Geng","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-2739-2881","authenticated-orcid":false,"given":"Jake Brandon","family":"Baldauf","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2706-2095","authenticated-orcid":false,"given":"Souradeep","family":"Dutta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9300-1787","authenticated-orcid":false,"given":"Chao","family":"Huang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3546-414X","authenticated-orcid":false,"given":"Ivan","family":"Ruchkin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,9,11]]},"reference":[{"key":"20_CR1","doi-asserted-by":"crossref","unstructured":"Agha, G., Palmskog, K.: A survey of statistical model checking. ACM Trans. Modeling Comput. Simul. 28 (2018,1), Publisher Copyright: 2018 ACM","DOI":"10.1145\/3158668"},{"key":"20_CR2","unstructured":"Althoff, M.: An introduction to CORA 2015. In: Proc. of the Workshop on Applied Verification for Continuous And Hybrid Systems, pp. 120-151 (2015)"},{"key":"20_CR3","unstructured":"Auer, A., Gauch, M., Klotz, D., Hochreiter, S.: Conformal prediction for time series with modern hopfield networks. In: Proceedings Of The 37th International Conference On Neural Information Processing Systems (2024)"},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"Bansal, S., Chen, M., Herbert, S.L., Tomlin, C.J.: Hamilton-jacobi reachability: a brief overview and recent advances. 2017 IEEE 56th Annual Conference on Decision and Control (CDC), pp. 2242\u20132253 (2017). https:\/\/api.semanticscholar.org\/CorpusID:35768454","DOI":"10.1109\/CDC.2017.8263977"},{"key":"20_CR5","doi-asserted-by":"crossref","unstructured":"Bansal, S., Tomlin, C.J.: Deepreach: a deep learning approach to high-dimensional reachability. In: 2021 IEEE International Conference on Robotics and Automation (ICRA), pp. 1817\u20131824. IEEE (2021)","DOI":"10.1109\/ICRA48506.2021.9561949"},{"key":"20_CR6","doi-asserted-by":"crossref","unstructured":"Bassan, S., Katz, G.: Towards formal xai: formally approximate minimal explanations of neural networks. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 187\u2013207. Springer (2023)","DOI":"10.1007\/978-3-031-30823-9_10"},{"key":"20_CR7","unstructured":"Brockman, G., Cheung, V., Pettersson, L., Schneider, J., Schulman, J., Tang, J., Zaremba, W.: OpenAI Gym (Jun 2016). http:\/\/arxiv.org\/abs\/1606.01540, arXiv:1606.01540 [cs]"},{"issue":"5","key":"20_CR8","doi-asserted-by":"publisher","first-page":"2692","DOI":"10.1109\/LRA.2023.3258719","volume":"8","author":"K Chakraborty","year":"2023","unstructured":"Chakraborty, K., Bansal, S.: Discovering closed-loop failures of vision-based controllers via reachability analysis. IEEE Robot. Automation Lett. 8(5), 2692\u20132699 (2023)","journal-title":"IEEE Robot. Automation Lett."},{"key":"20_CR9","doi-asserted-by":"crossref","unstructured":"Chen, X., \u00c1brah\u00e1m, E., Sankaranarayanan, S.: Flow*: An analyzer for non-linear hybrid systems. In: International Conference on Computer Aided Verification (2013)","DOI":"10.1007\/978-3-642-39799-8_18"},{"key":"20_CR10","doi-asserted-by":"crossref","unstructured":"Chen, X., Sankaranarayanan, S.: Reachability analysis for cyber-physical systems: Are we there yet? In: NASA Formal Methods Symposium, pp. 109-130 (2022)","DOI":"10.1007\/978-3-031-06773-0_6"},{"key":"20_CR11","doi-asserted-by":"crossref","unstructured":"Cleaveland, M., Lee, I., Pappas, G., Lindemann, L.: Conformal prediction regions for time series using linear complementarity programming. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol. 38, pp. 20984\u201320992 (2024)","DOI":"10.1609\/aaai.v38i19.30089"},{"key":"20_CR12","doi-asserted-by":"crossref","unstructured":"Cleaveland, M., Sokolsky, O., Lee, I., Ruchkin, I.: Conservative safety monitors of stochastic dynamical systems. In: Proc. of the NASA Formal Methods Conference, May 2023","DOI":"10.1007\/978-3-031-33170-1_9"},{"key":"20_CR13","doi-asserted-by":"crossref","unstructured":"Codevilla, F., M\u00fcller, M., L\u00f3pez, A., Koltun, V., Dosovitskiy, A.: End-to-end driving via conditional imitation learning. In: 2018 IEEE International Conference On Robotics And Automation (ICRA), pp. 4693-4700 (2018)","DOI":"10.1109\/ICRA.2018.8460487"},{"key":"20_CR14","doi-asserted-by":"crossref","unstructured":"Cofer, D., et al.: Run-time assurance for learning-based aircraft taxiing. In: 2020 AIAA\/IEEE 39th Digital Avionics Systems Conference (DASC), pp. 1\u20139 (2020)","DOI":"10.1109\/DASC50938.2020.9256581"},{"key":"20_CR15","doi-asserted-by":"publisher","unstructured":"Combettes, P.L., Pesquet, J.C.: Lipschitz Certificates for Layered Network Structures Driven by Averaged Activation Operators. SIAM Journal on Mathematics of Data Science 2(2), 529\u2013557 (Jan 2020). https:\/\/doi.org\/10.1137\/19M1272780, publisher: Society for Industrial and Applied Mathematics","DOI":"10.1137\/19M1272780"},{"issue":"4","key":"20_CR16","doi-asserted-by":"publisher","first-page":"485","DOI":"10.1109\/JPROC.2020.2976475","volume":"108","author":"L Deng","year":"2020","unstructured":"Deng, L., Li, G., Han, S., Shi, L., Xie, Y.: Model compression and hardware acceleration for neural networks: a comprehensive survey. Proc. IEEE 108(4), 485\u2013532 (2020)","journal-title":"Proc. IEEE"},{"key":"20_CR17","doi-asserted-by":"publisher","unstructured":"Dutta, S., et al.: Distributionally robust statistical verification with imprecise neural networks (Aug 2023). https:\/\/doi.org\/10.48550\/arXiv.2308.14815, arXiv:2308.14815 [cs]","DOI":"10.48550\/arXiv.2308.14815"},{"key":"20_CR18","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: demo abstract. In: Proceedings of the 22nd ACM International Conference On Hybrid Systems: Computation And Control, pp. 262\u2013263 (2019)","DOI":"10.1145\/3302504.3313351"},{"key":"20_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"446","DOI":"10.1007\/978-3-319-24953-7_32","volume-title":"Automated Technology for Verification and Analysis","author":"C Fan","year":"2015","unstructured":"Fan, C., Mitra, S.: Bounded verification with on-the-fly discrepancy computation. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) ATVA 2015. LNCS, vol. 9364, pp. 446\u2013463. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24953-7_32"},{"key":"20_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/978-3-319-63387-9_22","volume-title":"Computer Aided Verification","author":"C Fan","year":"2017","unstructured":"Fan, C., Qi, B., Mitra, S., Viswanathan, M.: DryVR: data-driven verification and compositional reasoning for automotive systems. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 441\u2013461. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_22"},{"key":"20_CR21","doi-asserted-by":"crossref","unstructured":"Fan, J., Huang, C., Li, W., Chen, X., Zhu, Q.: Towards verification-aware knowledge distillation for neural-network controlled systems: Invited paper. In: 2019 IEEE\/ACM International Conference on Computer-Aided Design (ICCAD), pp.\u00a01\u20138 (2019). https:\/\/api.semanticscholar.org\/CorpusID:209497572","DOI":"10.1109\/ICCAD45719.2019.8942059"},{"key":"20_CR22","doi-asserted-by":"crossref","unstructured":"Fannjiang, C., Bates, S., Angelopoulos, A., Listgarten, J., Jordan, M.: Conformal prediction under feedback covariate shift for biomolecular design. Proc. Natl. Acad. Sci. 119, e2204569119 (2022)","DOI":"10.1073\/pnas.2204569119"},{"key":"20_CR23","unstructured":"Fazlyab, M., Robey, A., Hassani, H., Morari, M., Pappas, G.: Efficient and accurate estimation of lipschitz constants for deep neural networks. In: Advances in Neural Information Processing Systems, vol.\u00a032. Curran Associates, Inc. (2019). https:\/\/proceedings.neurips.cc\/paper_files\/paper\/2019\/hash\/95e1533eb1b20a97777749fb94fdb944-Abstract.html"},{"key":"20_CR24","doi-asserted-by":"publisher","first-page":"1789","DOI":"10.1007\/s11263-021-01453-z","volume":"129","author":"J Gou","year":"2021","unstructured":"Gou, J., Yu, B., Maybank, S.J., Tao, D.: Knowledge distillation: a survey. Int. J. Comput. Vision 129, 1789\u20131819 (2021)","journal-title":"Int. J. Comput. Vision"},{"key":"20_CR25","unstructured":"Hinton, G., Vinyals, O., Dean, J.: Distilling the knowledge in a neural network. arXiv preprint arXiv:1503.02531 (2015)"},{"issue":"11","key":"20_CR26","doi-asserted-by":"publisher","first-page":"4205","DOI":"10.1109\/TCAD.2022.3197508","volume":"41","author":"C Hsieh","year":"2022","unstructured":"Hsieh, C., Li, Y., Sun, D., Joshi, K., Misailovic, S., Mitra, S.: Verifying controllers with vision-based perception using safe approximate abstractions. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 41(11), 4205\u20134216 (2022). https:\/\/doi.org\/10.1109\/TCAD.2022.3197508","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"20_CR27","doi-asserted-by":"crossref","unstructured":"Huang, C., Fan, J., Chen, X., Li, W., Zhu, Q.: Polar: A polynomial arithmetic framework for verifying neural-network controlled systems. In: International Symposium on Automated Technology for Verification and Analysis, pp. 414\u2013430. Springer (2022)","DOI":"10.1007\/978-3-031-19992-9_27"},{"issue":"5s","key":"20_CR28","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3358228","volume":"18","author":"C Huang","year":"2019","unstructured":"Huang, C., Fan, J., Li, W., Chen, X., Zhu, Q.: Reachnn: reachability analysis of neural-network controlled systems. ACM Trans. Embedded Comput. Syst. (TECS) 18(5s), 1\u201322 (2019)","journal-title":"ACM Trans. Embedded Comput. Syst. (TECS)"},{"key":"20_CR29","unstructured":"Fazlyab, M., Robey, A., Hassani, H., Morari, M., Pappas, G.: Efficient and accurate estimation of lipschitz constants for deep neural networks. In: Advances In Neural Information Processing Systems. 32 (2019)"},{"key":"20_CR30","doi-asserted-by":"crossref","unstructured":"Ivanov, R., Weimer, J., Alur, R., Pappas, G., Lee, I.: Verisig: verifying safety properties of hybrid systems with neural network controllers. In: Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation And Control, pp. 169-178 (2019)","DOI":"10.1145\/3302504.3311806"},{"issue":"9","key":"20_CR31","doi-asserted-by":"publisher","first-page":"574","DOI":"10.2514\/1.I011071","volume":"19","author":"SM Katz","year":"2022","unstructured":"Katz, S.M., Corso, A.L., Strong, C.A., Kochenderfer, M.J.: Verification of image-based neural network controllers using generative models. J. Aerospace Inf. Syst. 19(9), 574\u2013584 (2022)","journal-title":"J. Aerospace Inf. Syst."},{"key":"20_CR32","doi-asserted-by":"publisher","unstructured":"Khedr, H., Ferlez, J., Shoukry, Y.: Peregrinn: Penalized-relaxation greedy neural network verifier. In: Computer Aided Verification: 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part I, pp. 287-300 (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_13","DOI":"10.1007\/978-3-030-81685-8_13"},{"key":"20_CR33","unstructured":"Ladner, T., Althoff, M.: Specification-driven neural network reduction for scalable formal verification. arXiv preprint arXiv:2305.01932 (2023)"},{"key":"20_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-47166-2_1","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques","author":"KG Larsen","year":"2016","unstructured":"Larsen, K.G., Legay, A.: Statistical model checking: past, present, and future. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 3\u201315. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-47166-2_1"},{"key":"20_CR35","unstructured":"Lew, T., Janson, L., Bonalli, R., Pavone, M.: A Simple and Efficient Sampling-based Algorithm for General Reachability Analysis. In: Proceedings of the 4th Annual Learning for Dynamics and Control Conference. 168, pp. 1086\u20131099 (2022,6,23). https:\/\/proceedings.mlr.press\/v168\/lew22a.html"},{"key":"20_CR36","unstructured":"Lillicrap, T., Hunt, J., Pritzel, A., Heess, N., Erez, T., Tassa, Y., Silver, D., Wierstra, D.: Continuous control with deep reinforcement learning. CoRR. abs\/1509.02971 (2015). https:\/\/api.semanticscholar.org\/CorpusID:16326763"},{"key":"20_CR37","doi-asserted-by":"publisher","unstructured":"Lindemann, L., Qin, X., Deshmukh, J.V., Pappas, G.J.: Conformal prediction for stl runtime verification. In: Proceedings of the ACM\/IEEE 14th International Conference on Cyber-Physical Systems (with CPS-IoT Week 2023), pp. 142\u2013153. ICCPS \u201923, Association for Computing Machinery, New York (2023). https:\/\/doi.org\/10.1145\/3576841.3585927","DOI":"10.1145\/3576841.3585927"},{"key":"20_CR38","doi-asserted-by":"publisher","first-page":"201","DOI":"10.29007\/btv1","volume":"61","author":"DM Lopez","year":"2019","unstructured":"Lopez, D.M., Musau, P., Tran, H.D., Johnson, T.T.: Verification of closed-loop systems with neural network controllers. EPiC Series in Computing 61, 201\u2013210 (2019)","journal-title":"EPiC Series in Computing"},{"key":"20_CR39","doi-asserted-by":"crossref","unstructured":"Luo, R., Zhao, S., Kuck, J., Ivanovic, B., Savarese, S., Schmerling, E., Pavone, M.: Sample-efficient safety assurances using conformal prediction. In: International Workshop on the Algorithmic Foundations of Robotics, pp. 149\u2013169. Springer (2022)","DOI":"10.1007\/978-3-031-21090-7_10"},{"key":"20_CR40","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/978-3-030-35679-8_6","volume-title":"Advances on Robotic Item Picking","author":"E Matsumoto","year":"2020","unstructured":"Matsumoto, E., Saito, M., Kume, A., Tan, J.: End-to-end learning of object grasp poses in the amazon robotics challenge. In: Causo, A., Durham, J., Hauser, K., Okada, K., Rodriguez, A. (eds.) Advances on Robotic Item Picking, pp. 63\u201372. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-35679-8_6"},{"key":"20_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/978-3-030-85037-1_8","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"S Mohammadinejad","year":"2021","unstructured":"Mohammadinejad, S., Paulsen, B., Deshmukh, J.V., Wang, C.: DiffRNN: differential verification of recurrent neural networks. In: Dima, C., Shirmohammadi, M. (eds.) FORMATS 2021. LNCS, vol. 12860, pp. 117\u2013134. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-85037-1_8"},{"key":"20_CR42","doi-asserted-by":"crossref","unstructured":"Pan, Y., Cheng, C., Saigol, K., Lee, K., Yan, X., Theodorou, E., Boots, B.: Agile Autonomous Driving using End-to-End Deep Imitation Learning. Robotics: Science And Systems XIV (2017). https:\/\/api.semanticscholar.org\/CorpusID:53873353","DOI":"10.15607\/RSS.2018.XIV.056"},{"key":"20_CR43","doi-asserted-by":"crossref","unstructured":"P\u0103s\u0103reanu, C.S., Mangal, R., Gopinath, D., Getir\u00a0Yaman, S., Imrie, C., Calinescu, R., Yu, H.: Closed-loop analysis of vision-based autonomous systems: A case study. In: International Conference on Computer Aided Verification, pp. 289\u2013303. Springer (2023)","DOI":"10.1007\/978-3-031-37706-8_15"},{"key":"20_CR44","unstructured":"Qin, X., Hashemi, N., Lindemann, L., Deshmukh, J.V.: Conformance testing for stochastic cyber-physical systems. In: Conference on Formal Methods in Computer-Aided Design\u2013FMCAD 2023, p.\u00a0294 (2023)"},{"key":"20_CR45","doi-asserted-by":"publisher","unstructured":"Qin, X., Xia, Y., Zutshi, A., Fan, C., Deshmukh, J.V.: Statistical verification of cyber-physical systems using surrogate models and conformal inference. In: 2022 ACM\/IEEE 13th International Conference on Cyber-Physical Systems (ICCPS), pp. 116\u2013126 (2022). https:\/\/doi.org\/10.1109\/ICCPS54341.2022.00017","DOI":"10.1109\/ICCPS54341.2022.00017"},{"key":"20_CR46","doi-asserted-by":"publisher","unstructured":"Ruchkin, I., Cleaveland, M., Ivanov, R., Lu, P., Carpenter, T., Sokolsky, O., Lee, I.: Confidence composition for monitors of verification assumptions. In: ACM\/IEEE 13th Intl. Conf. on Cyber-Physical Systems (ICCPS), pp. 1\u201312, May 2022. https:\/\/doi.org\/10.1109\/ICCPS54341.2022.00007","DOI":"10.1109\/ICCPS54341.2022.00007"},{"key":"20_CR47","doi-asserted-by":"publisher","unstructured":"Santa\u00a0Cruz, U., Shoukry, Y.: Nnlander-verif: a neural network formal verification framework for vision-based autonomous aircraft landing. Springer, Heidelberg (2022). https:\/\/doi.org\/10.1007\/978-3-031-06773-0_11","DOI":"10.1007\/978-3-031-06773-0_11"},{"key":"20_CR48","unstructured":"Shafer, G., Vovk, V.: A Tutorial on Conformal Prediction. J. Mach. Learn. Res. 9, 371\u2013421 (2008). http:\/\/dl.acm.org\/citation.cfm?id=1390681.1390693"},{"key":"20_CR49","doi-asserted-by":"publisher","unstructured":"Stocco, A., Nunes, P.J., D\u2019Amorim, M., Tonella, P.: Thirdeye: Attention maps for safe autonomous driving systems. In: Proceedings of the 37th IEEE\/ACM International Conference on Automated Software Engineering, ASE 2022. Association for Computing Machinery, New York (2023). https:\/\/doi.org\/10.1145\/3551349.3556968","DOI":"10.1145\/3551349.3556968"},{"key":"20_CR50","unstructured":"Szegedy, C., Zaremba, W., Sutskever, I., Bruna, J., Erhan, D., Goodfellow, I., Fergus, R.: Intriguing properties of neural networks. In: International Conference on Learning Representations (2014)"},{"key":"20_CR51","doi-asserted-by":"crossref","unstructured":"Teeti, I., Khan, S., Shahbaz, A., Bradley, A., Cuzzolin, F.: Vision-based Intention and Trajectory Prediction in Autonomous Vehicles: A Survey, vol.\u00a06, pp. 5630\u20135637 (Jul 2022). https:\/\/www.ijcai.org\/proceedings\/2022\/785, iSSN: 1045-0823","DOI":"10.24963\/ijcai.2022\/785"},{"key":"20_CR52","unstructured":"Topcu, U., Bliss, N., Cooke, N., Cummings, M., Llorens, A., Shrobe, H., Zuck, L.: Assured Autonomy: Path Toward Living With Autonomous Systems We Can Trust, October 2020. http:\/\/arxiv.org\/abs\/2010.14443, arXiv:2010.14443 [cs]"},{"key":"20_CR53","doi-asserted-by":"crossref","unstructured":"Tran, H.D., Manzanas\u00a0Lopez, D., Musau, P., Yang, X., Nguyen, L.V., Xiang, W., Johnson, T.T.: Star-based reachability analysis of deep neural networks. In: Formal Methods\u2013The Next 30 Years: Third World Congress, FM 2019, Porto, Portugal, October 7\u201311, 2019, Proceedings 3, pp. 670\u2013686. Springer (2019)","DOI":"10.1007\/978-3-030-30942-8_39"},{"key":"20_CR54","doi-asserted-by":"crossref","unstructured":"Tran, H., et al.: NNV: the neural network verification tool for deep neural networks and learning-enabled cyber-physical systems. In: International Conference on Computer Aided Verification, pp. 3-17 (2020)","DOI":"10.1007\/978-3-030-53288-8_1"},{"key":"20_CR55","unstructured":"Vovk, V., Gammerman, A., Shafer, G.: Algorithmic Learning in a Random World. Springer, New York, 2005 edition edn. (2005)"},{"key":"20_CR56","doi-asserted-by":"crossref","unstructured":"Xiang, W., Shao, Z.: Approximate bisimulation relations for neural networks and application to assured neural network compression. In: 2022 American Control Conference (ACC), pp. 3248\u20133253. IEEE (2022)","DOI":"10.23919\/ACC53348.2022.9867845"},{"key":"20_CR57","doi-asserted-by":"crossref","unstructured":"Xiang, W., Shao, Z.: Safety verification of neural network control systems using guaranteed neural network model reduction. In: 2022 IEEE 61st Conference on Decision and Control (CDC), pp. 1521\u20131526. IEEE (2022)","DOI":"10.1109\/CDC51059.2022.9992984"},{"key":"20_CR58","unstructured":"Xu, C., Xie, Y.: Conformal prediction interval for dynamic time-series. In: Proceedings of the 38th International Conference on Machine Learning, pp. 11559\u201311569. PMLR, July 2021. https:\/\/proceedings.mlr.press\/v139\/xu21h.html, iSSN: 2640-3498"},{"key":"20_CR59","doi-asserted-by":"publisher","unstructured":"Xue, B., Zhang, M., Easwaran, A., Li, Q.: Pac model checking of black-box continuous-time dynamical systems. IEEE Trans. Comput.-Aided Des. Integrated Circuits Syst. 39 (07 2020). https:\/\/doi.org\/10.1109\/TCAD.2020.3012251","DOI":"10.1109\/TCAD.2020.3012251"},{"key":"20_CR60","doi-asserted-by":"crossref","unstructured":"Zarei, M., Wang, Y., Pajic, M.: Statistical verification of learning-based cyber-physical systems. In: Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control, HSCC 2020. Association for Computing Machinery, New York (2020). https:\/\/doi.org\/10.1145\/3365365.3382209","DOI":"10.1145\/3365365.3382209"},{"key":"20_CR61","doi-asserted-by":"publisher","unstructured":"Zhang, M., Zhang, Y., Zhang, L., Liu, C., Khurshid, S.: Deeproad: Gan-based metamorphic testing and input validation framework for autonomous driving systems. In: Proceedings of the 33rd ACM\/IEEE International Conference on Automated Software Engineering, pp. 132-142. ASE 2018. Association for Computing Machinery, New York, NY, USA (2018). https:\/\/doi.org\/10.1145\/3238147.3238187","DOI":"10.1145\/3238147.3238187"},{"key":"20_CR62","doi-asserted-by":"crossref","unstructured":"Wang, Y., Zhou, W., Fan, J., Wang, Z., Li, J., Chen, X., Huang, C., Li, W. and Zhu, Q.: Polar-express: Efficient and precise formal reachability analysis of neural-network controlled systems. In: IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems. (2023)","DOI":"10.1109\/TCAD.2023.3331215"},{"key":"20_CR63","doi-asserted-by":"publisher","first-page":"634","DOI":"10.3390\/aerospace9110634","volume":"9","author":"L Xin","year":"2022","unstructured":"Xin, L., Tang, Z., Gai, W., Liu, H.: Vision-based autonomous landing for the UAV: A review. Aerospace 9, 634 (2022)","journal-title":"Aerospace"},{"key":"20_CR64","doi-asserted-by":"crossref","unstructured":"Tang, C., Lai, Y.: Deep reinforcement learning automatic landing control of fixed-wing aircraft using deep deterministic policy gradient. In: 2020 International Conference On Unmanned Aircraft Systems (ICUAS), pp. 1-9 (2020)","DOI":"10.1109\/ICUAS48674.2020.9213987"},{"key":"20_CR65","doi-asserted-by":"publisher","first-page":"973","DOI":"10.1108\/AEAT-11-2017-0250","volume":"90","author":"M Oszust","year":"2018","unstructured":"Oszust, M., et al.: A vision-based method for supporting autonomous aircraft landing. Aircraft Eng. Aerospace Technol. 90, 973\u2013982 (2018)","journal-title":"Aircraft Eng. Aerospace Technol."},{"key":"20_CR66","doi-asserted-by":"crossref","unstructured":"Menghi, C., Nejati, S., Briand, L., Parache, Y.: Approximation-refinement testing of compute-intensive cyber-physical models: an approach based on system identification. In: 2020 IEEE\/ACM 42nd International Conference On Software Engineering (ICSE), pp. 372\u2013384 (2020)","DOI":"10.1145\/3377811.3380370"},{"key":"20_CR67","doi-asserted-by":"crossref","unstructured":"Geng, Y., Baldauf, J. B., Dutta, S., Huang, C., Ruchkin, I.: Bridging Dimensions: Confident Reachability for High-Dimensional Controllers. 2024. arXiv preprint arXiv:2311.04843. https:\/\/arxiv.org\/abs\/2311.04843","DOI":"10.1007\/978-3-031-71162-6_20"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-71162-6_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,27]],"date-time":"2024-11-27T23:02:01Z","timestamp":1732748521000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-71162-6_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,11]]},"ISBN":["9783031711619","9783031711626"],"references-count":67,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-71162-6_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,9,11]]},"assertion":[{"value":"11 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Milan","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","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":"9 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 September 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.fm24.polimi.it\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}