{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,8]],"date-time":"2026-10-08T11:43:10Z","timestamp":1791459790687,"version":"4.3.4"},"publisher-location":"Cham","reference-count":87,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031757778","type":"print"},{"value":"9783031757785","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,11,18]],"date-time":"2024-11-18T00:00:00Z","timestamp":1731888000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,11,18]],"date-time":"2024-11-18T00:00:00Z","timestamp":1731888000000},"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":[[2025]]},"DOI":"10.1007\/978-3-031-75778-5_5","type":"book-chapter","created":{"date-parts":[[2024,11,17]],"date-time":"2024-11-17T12:09:17Z","timestamp":1731845357000},"page":"89-108","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Formal Verification Techniques for\u00a0Vision-Based Autonomous Systems \u2013 A Survey"],"prefix":"10.1007","author":[{"given":"Sayan","family":"Mitra","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Corina","family":"P\u0103s\u0103reanu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Pavithra","family":"Prabhakar","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sanjit A.","family":"Seshia","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ravi","family":"Mangal","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yangge","family":"Li","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Christopher","family":"Watson","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Divya","family":"Gopinath","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Huafeng","family":"Yu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,11,18]]},"reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"Alshiekh, M., Bloem, R., Ehlers, R., K\u00f6nighofer, B., Niekum, S., Topcu, U.: Safe reinforcement learning via shielding. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol.\u00a032 (2018)","DOI":"10.1609\/aaai.v32i1.11797"},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R.: Formal verification of hybrid systems. In: Proceedings of the Ninth ACM International Conference on Embedded Software, pp. 273\u2013278 (2011)","DOI":"10.1145\/2038642.2038685"},{"key":"5_CR3","doi-asserted-by":"publisher","unstructured":"Ames, A.D., Coogan, S., Egerstedt, M., Notomista, G., Sreenath, K., Tabuada, P.: Control barrier functions: Theory and applications. In: 2019 18th European Control Conference (ECC), pp. 3420\u20133431 (2019). https:\/\/doi.org\/10.23919\/ECC.2019.8796030","DOI":"10.23919\/ECC.2019.8796030"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"ArjomandBigdeli, A., Mata, A., Bak, S.: Verification of neural network control systems in continuous time. In: 7th Symposium on AI Verification (SAIV) (2024)","DOI":"10.1007\/978-3-031-65112-0_5"},{"key":"5_CR5","doi-asserted-by":"publisher","unstructured":"Astorga, A., Hsieh, C., Madhusudan, P., Mitra, S.: Perception contracts for safety of ML-enabled systems. Proc. ACM Program. Lang. 7(OOPSLA2), 2196\u20132223 (2023). https:\/\/doi.org\/10.1145\/3622875","DOI":"10.1145\/3622875"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"Badithela, A., Wongpiromsarn, T., Murray, R.M.: Leveraging classification metrics for quantitative system-level analysis with temporal logic specifications. In: 2021 60th IEEE Conference on Decision and Control (CDC), pp. 564\u2013571. IEEE (2021)","DOI":"10.1109\/CDC45484.2021.9683611"},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"Badithela, A., Wongpiromsarn, T., Murray, R.M.: Evaluation metrics of object detection for quantitative system-level analysis of safety-critical autonomous systems. In: 2023 IEEE\/RSJ International Conference on Intelligent Robots and Systems (IROS), pp. 8651\u20138658. IEEE (2023)","DOI":"10.1109\/IROS55552.2023.10342465"},{"key":"5_CR8","doi-asserted-by":"publisher","unstructured":"Bogomolov, S., et al.: Assume-guarantee abstraction refinement meets hybrid systems. In: Yahav, E. (ed.) Hardware and Software: Verification and Testing - 10th International Haifa Verification Conference, HVC 2014, Haifa, Israel, 18\u201320 November 2014, Proceedings. LNCS, vol.\u00a08855, pp. 116\u2013131. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-13338-6_10","DOI":"10.1007\/978-3-319-13338-6_10"},{"key":"5_CR9","unstructured":"Bullo, F.: Contraction Theory for Dynamical Systems, 1.1 edn. Kindle Direct Publishing (2023)"},{"key":"5_CR10","unstructured":"Cai, F., Fan, C., Bak, S.: Scalable surrogate verification of image-based neural network control systems using composition and unrolling (2024)"},{"key":"5_CR11","unstructured":"Calinescu, R., Imrie, C., Mangal, R., P\u0103s\u0103reanu, C., Santana, M.A., V\u00e1zquez, G.: Discrete-event controller synthesis for autonomous systems with deep-learning perception components. arXiv preprint arXiv:2202.03360 (2022)"},{"key":"5_CR12","doi-asserted-by":"publisher","unstructured":"Calinescu, R., et al.: Controller synthesis for autonomous systems with deep-learning perception components. IEEE Trans. Softw. Eng. 1\u201322 (2024). https:\/\/doi.org\/10.1109\/TSE.2024.3385378","DOI":"10.1109\/TSE.2024.3385378"},{"key":"5_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-642-39799-8_18","volume-title":"Computer Aided Verification","author":"X Chen","year":"2013","unstructured":"Chen, X., \u00c1brah\u00e1m, E., Sankaranarayanan, S.: Flow*: an analyzer for non-linear hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 258\u2013263. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_18"},{"key":"5_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-540-24611-4_5","volume-title":"Validation of Stochastic Systems","author":"F Ciesinski","year":"2004","unstructured":"Ciesinski, F., Gr\u00f6\u00dfer, M.: On probabilistic computation tree logic. In: Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P., Siegle, M. (eds.) Validation of Stochastic Systems. LNCS, vol. 2925, pp. 147\u2013188. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24611-4_5"},{"key":"5_CR15","doi-asserted-by":"publisher","unstructured":"Cosner, R.K., Singletary, A.W., Taylor, A.J., Molnar, T.G., Bouman, K.L., Ames, A.D.: Measurement-robust control barrier functions: certainty in safety with uncertainty in state. In: 2021 IEEE\/RSJ International Conference on Intelligent Robots and Systems (IROS), pp. 6286\u20136291 (2021). https:\/\/doi.org\/10.1109\/IROS51168.2021.9636584","DOI":"10.1109\/IROS51168.2021.9636584"},{"key":"5_CR16","doi-asserted-by":"publisher","unstructured":"Cruz, U.S., Shoukry, Y.: Certified vision-based state estimation for autonomous landing systems using reachability analysis. In: 2023 62nd IEEE Conference on Decision and Control (CDC), pp. 6052\u20136057 (2023). https:\/\/doi.org\/10.1109\/CDC49753.2023.10384107","DOI":"10.1109\/CDC49753.2023.10384107"},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"Dawson, C., Gao, S., Fan, C.: Safe control with learned certificates: a survey of neural Lyapunov, barrier, and contraction methods. arXiv preprint arXiv:2202.11762 (2022)","DOI":"10.1109\/TRO.2022.3232542"},{"issue":"2","key":"5_CR18","doi-asserted-by":"publisher","first-page":"1904","DOI":"10.1109\/LRA.2022.3141657","volume":"7","author":"C Dawson","year":"2022","unstructured":"Dawson, C., Lowenkamp, B., Goff, D., Fan, C.: Learning safe, generalizable perception-based hybrid control with certificates. IEEE Robot. Autom. Lett. 7(2), 1904\u20131911 (2022)","journal-title":"IEEE Robot. Autom. Lett."},{"key":"5_CR19","unstructured":"Dean, S., Taylor, A., Cosner, R., Recht, B., Ames, A.: Guaranteeing safety of learned perception modules via measurement-robust control barrier functions. In: Conference on Robot Learning, pp. 654\u2013670. PMLR (2021)"},{"key":"5_CR20","unstructured":"Dosovitskiy, A., Ros, G., Codevilla, F., Lopez, A., Koltun, V.: CARLA: an open urban driving simulator. In: Proceedings of the 1st Annual Conference on Robot Learning, pp. 1\u201316 (2017)"},{"key":"5_CR21","doi-asserted-by":"crossref","unstructured":"Dreossi, T., Donze, A., Seshia, S.A.: Compositional falsification of cyber-physical systems with machine learning components. In: Proceedings of the NASA Formal Methods Conference (NFM), pp. 357\u2013372, May 2017","DOI":"10.1007\/978-3-319-57288-8_26"},{"issue":"4","key":"5_CR22","doi-asserted-by":"publisher","first-page":"1031","DOI":"10.1007\/s10817-018-09509-5","volume":"63","author":"T Dreossi","year":"2019","unstructured":"Dreossi, T., Donz\u00e9, A., Seshia, S.A.: Compositional falsification of cyber-physical systems with machine learning components. J. Autom. Reason. 63(4), 1031\u20131053 (2019)","journal-title":"J. Autom. Reason."},{"key":"5_CR23","doi-asserted-by":"crossref","unstructured":"Dreossi, T., et al.: VerifAI: a toolkit for the formal design and analysis of artificial intelligence-based systems. In: 31st International Conference on Computer Aided Verification (CAV), July 2019","DOI":"10.1007\/978-3-030-25540-4_25"},{"key":"5_CR24","doi-asserted-by":"publisher","unstructured":"Dutta, S., Chen, X., Sankaranarayanan, S.: Reachability analysis for neural feedback systems using regressive polynomial rule inference. In: Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2019, pp. 157\u2013168. Association for Computing Machinery, New York, NY, USA (2019). https:\/\/doi.org\/10.1145\/3302504.3311807","DOI":"10.1145\/3302504.3311807"},{"key":"5_CR25","doi-asserted-by":"publisher","first-page":"537","DOI":"10.1007\/978-3-030-59152-6_30","volume-title":"Automated Technology for Verification and Analysis","author":"J Fan","year":"2020","unstructured":"Fan, J., Huang, C., Chen, X., Li, W., Zhu, Q.: ReachNN*: a tool for reachability analysis of neural-network controlled systems. In: Hung, D.V., Sokolsky, O. (eds.) Automated Technology for Verification and Analysis, pp. 537\u2013542. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-59152-6_30"},{"key":"5_CR26","doi-asserted-by":"crossref","unstructured":"Fremont, D.J., Chiu, J., Margineantu, D.D., Osipychev, D., Seshia, S.A.: Formal analysis and redesign of a neural network-based aircraft taxiing system with VerifAI. In: 32nd International Conference on Computer Aided Verification (CAV), July 2020","DOI":"10.1007\/978-3-030-53288-8_6"},{"key":"5_CR27","doi-asserted-by":"crossref","unstructured":"Fremont, D.J., Dreossi, T., Ghosh, S., Yue, X., Sangiovanni-Vincentelli, A.L., Seshia, S.A.: Scenic: a language for scenario specification and scene generation. In: Proceedings of the 40th Annual ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), June 2019","DOI":"10.1145\/3314221.3314633"},{"key":"5_CR28","doi-asserted-by":"crossref","unstructured":"Fremont, D.J., et al.: Scenic: a language for scenario specification and data generation. Mach. Learn. J. (2022)","DOI":"10.1007\/s10994-021-06120-5"},{"key":"5_CR29","doi-asserted-by":"crossref","unstructured":"Fremont, D.J., et al.: Formal scenario-based testing of autonomous vehicles: from simulation to the real world. In: 23rd IEEE International Conference on Intelligent Transportation Systems (ITSC), September 2020","DOI":"10.1109\/ITSC45102.2020.9294368"},{"key":"5_CR30","doi-asserted-by":"crossref","unstructured":"Ghosh, S., Pant, Y.V., Ravanbakhsh, H., Seshia, S.A.: Counterexample-guided synthesis of perception models and control. In: American Control Conference (ACC), pp. 3447\u20133454. IEEE (2021)","DOI":"10.23919\/ACC50511.2021.9482896"},{"key":"5_CR31","doi-asserted-by":"publisher","unstructured":"Giannakopoulou, D., Pasareanu, C.S., Barringer, H.: Assumption generation for software component verification. In: 17th IEEE International Conference on Automated Software Engineering (ASE 2002), 23\u201327 September 2002, Edinburgh, Scotland, UK, pp. 3\u201312. IEEE Computer Society (2002). https:\/\/doi.org\/10.1109\/ASE.2002.1114984","DOI":"10.1109\/ASE.2002.1114984"},{"key":"5_CR32","doi-asserted-by":"crossref","unstructured":"Grigorescu, S.M., Trasnea, B., Cocias, T.T., Macesanu, G.: A survey of deep learning techniques for autonomous driving. CoRR abs\/1910.07738 (2019)","DOI":"10.1002\/rob.21918"},{"key":"5_CR33","doi-asserted-by":"publisher","unstructured":"Habeeb, P., Deka, N., D\u2019Souza, D., Lodaya, K., Prabhakar, P.: Verification of camera-based autonomous systems. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 42(10), 3450\u20133463 (2023). https:\/\/doi.org\/10.1109\/TCAD.2023.3240131","DOI":"10.1109\/TCAD.2023.3240131"},{"key":"5_CR34","doi-asserted-by":"crossref","unstructured":"Habeeb, P., D\u2019Souza, D., Lodaya, K., Prabhakar, P.: Interval image abstraction for verification of camera-based autonomous systems. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. (2024)","DOI":"10.1109\/TCAD.2024.3448306"},{"key":"5_CR35","doi-asserted-by":"crossref","unstructured":"Habeeb, P., Gupta, L., Prabhakar, P.: Approximate conformance checking for closed-loop systems with neural network controllers. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. (2024)","DOI":"10.1109\/TCAD.2024.3445813"},{"key":"5_CR36","doi-asserted-by":"crossref","unstructured":"Habeeb, P., Prabhakar, P.: Approximate conformance verification of deep neural networks. NASA Formal Methods (2024)","DOI":"10.1007\/978-3-031-60698-4_13"},{"issue":"4","key":"5_CR37","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/s10009-021-00633-z","volume":"24","author":"C Hensel","year":"2022","unstructured":"Hensel, C., Junges, S., Katoen, J.P., Quatmann, T., Volk, M.: The probabilistic model checker Storm. Int. J. Softw. Tools Technol. Transfer 24(4), 589\u2013610 (2022)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"5_CR38","doi-asserted-by":"crossref","unstructured":"Hsieh, C., Koh, Y., Li, Y., Mitra, S.: Assuring safety of vision-based swarm formation control. In: American Control Conference (ACC) (2024)","DOI":"10.23919\/ACC60939.2024.10644491"},{"key":"5_CR39","doi-asserted-by":"publisher","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","DOI":"10.1109\/TCAD.2022.3197508"},{"key":"5_CR40","doi-asserted-by":"publisher","unstructured":"Huang, C., Fan, J., Chen, X., Li, W., Zhu, Q.: POLAR: a polynomial arithmetic framework for verifying neural-network controlled systems. In: Automated Technology for Verification and Analysis: 20th International Symposium, ATVA 2022, Virtual Event, 25\u201328 October 2022, Proceedings, pp. 414\u2013430. Springer, Heidelberg (2022). https:\/\/doi.org\/10.1007\/978-3-031-19992-9_27","DOI":"10.1007\/978-3-031-19992-9_27"},{"key":"5_CR41","doi-asserted-by":"publisher","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), 1\u201322 (2019). https:\/\/doi.org\/10.1145\/3358228","DOI":"10.1145\/3358228"},{"key":"5_CR42","doi-asserted-by":"publisher","first-page":"100270","DOI":"10.1016\/j.cosrev.2020.100270","volume":"37","author":"X Huang","year":"2020","unstructured":"Huang, X., et al.: A survey of safety and trustworthiness of deep neural networks: verification, testing, adversarial attack and defence, and interpretability. Comput. Sci. Rev. 37, 100270 (2020)","journal-title":"Comput. Sci. Rev."},{"key":"5_CR43","doi-asserted-by":"publisher","unstructured":"Hunt, N., Fulton, N., Magliacane, S., Hoang, T.N., Das, S., Solar-Lezama, A.: Verifiably safe exploration for end-to-end reinforcement learning. In: Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control, HSCC 2021. Association for Computing Machinery, New York, NY, USA (2021). https:\/\/doi.org\/10.1145\/3447928.3456653","DOI":"10.1145\/3447928.3456653"},{"key":"5_CR44","unstructured":"Incer, I., et\u00a0al.: Pacti: scaling assume-guarantee reasoning for system analysis and design. arXiv preprint arXiv:2303.17751 (2023)"},{"key":"5_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-030-81685-8_11","volume-title":"Computer Aided Verification","author":"R Ivanov","year":"2021","unstructured":"Ivanov, R., Carpenter, T., Weimer, J., Alur, R., Pappas, G., Lee, I.: Verisig 2.0: verification of neural network controllers using Taylor model preconditioning. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 249\u2013262. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_11"},{"issue":"1","key":"5_CR46","first-page":"1","volume":"20","author":"R Ivanov","year":"2020","unstructured":"Ivanov, R., Carpenter, T.J., Weimer, J., Alur, R., Pappas, G.J., Lee, I.: Verifying the safety of autonomous systems with neural network controllers. ACM Trans. Embed. Comput. Syst. (TECS) 20(1), 1\u201326 (2020)","journal-title":"ACM Trans. Embed. Comput. Syst. (TECS)"},{"issue":"5s","key":"5_CR47","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3477023","volume":"20","author":"R Ivanov","year":"2021","unstructured":"Ivanov, R., Jothimurugan, K., Hsu, S., Vaidya, S., Alur, R., Bastani, O.: Compositional learning and verification of neural network controllers. ACM Trans. Embed. Comput. Syst. (TECS) 20(5s), 1\u201326 (2021)","journal-title":"ACM Trans. Embed. Comput. Syst. (TECS)"},{"key":"5_CR48","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: Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, pp. 169\u2013178 (2019)","DOI":"10.1145\/3302504.3311806"},{"key":"5_CR49","doi-asserted-by":"publisher","unstructured":"Kadron, I.B., Gopinath, D., Pasareanu, C.S., Yu, H.: Case study: analysis of autonomous center line tracking neural networks. In: Bloem, R., Dimitrova, R., Fan, C., Sharygina, N. (eds.) Software Verification - 13th International Conference, VSTTE 2021, New Haven, CT, USA, 18\u201319 October 2021, and 14th International Workshop, NSV 2021, Los Angeles, CA, USA, 18\u201319 July 2021, Revised Selected Papers. LNCS, pp. 104\u2013121. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-95561-8_7","DOI":"10.1007\/978-3-030-95561-8_7"},{"key":"5_CR50","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"},{"issue":"9","key":"5_CR51","first-page":"574","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. Aerosp. Inf. Syst. 19(9), 574\u2013584 (2022)","journal-title":"J. Aerosp. Inf. Syst."},{"key":"5_CR52","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-031-33170-1_2","volume-title":"NASA Formal Methods","author":"N Kochdumper","year":"2023","unstructured":"Kochdumper, N., Schilling, C., Althoff, M., Bak, S.: Open- and closed-loop neural network verification using polynomial zonotopes. In: Rozier, K.Y., Chaudhuri, S. (eds.) NASA Formal Methods, pp. 16\u201336. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-33170-1_2"},{"key":"5_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"key":"5_CR54","unstructured":"Laminar Research: X-Plane (2023). https:\/\/www.x-plane.com"},{"key":"5_CR55","unstructured":"Li, Y., Yang, B.C., Jia, Y., Zhuang, D., Mitra, S.: Refining perception contracts: case studies in vision-based safe auto-landing (2023)"},{"key":"5_CR56","doi-asserted-by":"publisher","unstructured":"Li, Y., Zhu, H., Braught, K., Shen, K., Mitra, S.: Verse: a Python library for reasoning about multi-agent hybrid system scenarios. In: Enea, C., Lal, A. (eds.) Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, 17\u201322 July 2023, Proceedings, Part I. LNCS, vol. 13964, pp. 351\u2013364. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-37706-8_18","DOI":"10.1007\/978-3-031-37706-8_18"},{"key":"5_CR57","doi-asserted-by":"crossref","unstructured":"Lohmiller, W., Slotine, J.J.E.: On contraction analysis for non-linear systems. Automatica (1998)","DOI":"10.1016\/S0005-1098(98)00019-3"},{"key":"5_CR58","doi-asserted-by":"publisher","unstructured":"Lopez, D.M., Choi, S.W., Tran, H.D., Johnson, T.T.: NNV 2.0: the neural network verification tool. In: Enea, C., Lal, A. (eds.) Computer Aided Verification, pp. 397\u2013412. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-37703-7_19","DOI":"10.1007\/978-3-031-37703-7_19"},{"key":"5_CR59","unstructured":"Mitra, S.: Verifying Cyber-Physical Systems: A Path to Safe Autonomy. The MIT Press, Cambridge (2021)"},{"key":"5_CR60","doi-asserted-by":"publisher","unstructured":"Naik, N., Nuzzo, P.: Robustness contracts for scalable verification of neural network-enabled cyber-physical systems. In: 2020 18th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE), pp. 1\u201312 (2020). https:\/\/doi.org\/10.1109\/MEMOCODE51338.2020.9315118","DOI":"10.1109\/MEMOCODE51338.2020.9315118"},{"key":"5_CR61","doi-asserted-by":"publisher","unstructured":"Pasareanu, C.S., Giannakopoulou, D., Bobaru, M.G., Cobleigh, J.M., Barringer, H.: Learning to divide and conquer: applying the l* algorithm to automate assume-guarantee reasoning. Formal Methods Syst. Des. 32(3), 175\u2013205 (2008). https:\/\/doi.org\/10.1007\/s10703-008-0049-6","DOI":"10.1007\/s10703-008-0049-6"},{"key":"5_CR62","unstructured":"Pasareanu, C.S., Gopinath, D., Yu, H.: Compositional verification for autonomous systems with deep learning components. CoRR abs\/1810.08303 (2018). http:\/\/arxiv.org\/abs\/1810.08303"},{"key":"5_CR63","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/978-3-031-37706-8_15","volume-title":"Computer Aided Verification","author":"CS P\u0103s\u0103reanu","year":"2023","unstructured":"P\u0103s\u0103reanu, C.S., et al.: Closed-loop analysis of vision-based autonomous systems: a case study. In: Enea, C., Lal, A. (eds.) Computer Aided Verification, pp. 289\u2013303. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-37706-8_15"},{"key":"5_CR64","doi-asserted-by":"publisher","unstructured":"Pasareanu, C.S., Mangal, R., Gopinath, D., Yu, H.: Assumption generation for learning-enabled autonomous systems. In: Katsaros, P., Nenzi, L. (eds.) Runtime Verification - 23rd International Conference, RV 2023, Thessaloniki, Greece, 3\u20136 October 2023, Proceedings. LNCS, vol. 14245, pp. 3\u201322. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-44267-4_1","DOI":"10.1007\/978-3-031-44267-4_1"},{"key":"5_CR65","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1007\/11730637_38","volume-title":"Hybrid Systems: Computation and Control","author":"A Podelski","year":"2006","unstructured":"Podelski, A., Wagner, S.: Model checking of hybrid systems: from reachability towards stability. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol. 3927, pp. 507\u2013521. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11730637_38"},{"key":"5_CR66","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/978-3-540-24743-2_32","volume-title":"Hybrid Systems: Computation and Control","author":"S Prajna","year":"2004","unstructured":"Prajna, S., Jadbabaie, A.: Safety verification of hybrid systems using barrier certificates. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 477\u2013492. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24743-2_32"},{"key":"5_CR67","unstructured":"Qin, Z., Zhang, K., Chen, Y., Chen, J., Fan, C.: Learning safe multi-agent control with decentralized neural barrier certificates. In: International Conference on Learning Representations (2021). https:\/\/openreview.net\/forum?id=P6_q1BRxY8Q"},{"key":"5_CR68","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/978-3-031-06773-0_11","volume-title":"NASA Formal Methods","author":"U Santa Cruz","year":"2022","unstructured":"Santa Cruz, U., Shoukry, Y.: NNLander-VerIF: a neural network formal verification framework for vision-based autonomous aircraft landing. In: Deshmukh, J.V., Havelund, K., Perez, I. (eds.) NASA Formal Methods, pp. 213\u2013230. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-06773-0_11"},{"key":"5_CR69","doi-asserted-by":"publisher","unstructured":"Schilling, C., Forets, M., Guadalupe, S.: Verification of neural-network control systems by integrating Taylor models and zonotopes. Proc. AAAI Conf. Artif. Intell. 36(7), 8169\u20138177 (2022). https:\/\/doi.org\/10.1609\/aaai.v36i7.20790","DOI":"10.1609\/aaai.v36i7.20790"},{"issue":"7","key":"5_CR70","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1145\/3503914","volume":"65","author":"SA Seshia","year":"2022","unstructured":"Seshia, S.A., Sadigh, D., Sastry, S.S.: Toward verified artificial intelligence. Commun. ACM 65(7), 46\u201355 (2022)","journal-title":"Commun. ACM"},{"key":"5_CR71","doi-asserted-by":"crossref","unstructured":"Sun, D., Yang, B., Mitra, S.: Learning-based inverse perception contracts and applications. In: International Conference on Robotics and Automation (2024)","DOI":"10.1109\/ICRA57147.2024.10610329"},{"key":"5_CR72","doi-asserted-by":"publisher","unstructured":"Sun, X., Khedr, H., Shoukry, Y.: Formal verification of neural network controlled autonomous systems. In: Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2019, pp. 147\u2013156. Association for Computing Machinery, New York, NY, USA (2019). https:\/\/doi.org\/10.1145\/3302504.3311802","DOI":"10.1145\/3302504.3311802"},{"key":"5_CR73","unstructured":"Tabernik, D., Skocaj, D.: Deep learning for large-scale traffic-sign detection and recognition. CoRR abs\/1904.00649 (2019)"},{"key":"5_CR74","doi-asserted-by":"crossref","unstructured":"Tong, M., Dawson, C., Fan, C.: Enforcing safety for vision-based controllers via control barrier functions and neural radiance fields. arXiv preprint arXiv:2209.12266 (2022)","DOI":"10.1109\/ICRA48891.2023.10161482"},{"key":"5_CR75","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/978-3-030-88494-9_19","volume-title":"Runtime Verification","author":"H Torfah","year":"2021","unstructured":"Torfah, H., Junges, S., Fremont, D.J., Seshia, S.A.: Formal analysis of AI-based autonomy: from modeling to runtime assurance. In: Feng, L., Fisman, D. (eds.) RV 2021. LNCS, vol. 12974, pp. 311\u2013330. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-88494-9_19"},{"key":"5_CR76","doi-asserted-by":"crossref","unstructured":"Torfah, H., Xie, C., Junges, S., Vazquez-Chanlatte, M., Seshia, S.A.: Learning monitorable operational design domains for assured autonomy. In: Proceedings of the International Symposium on Automated Technology for Verification and Analysis (ATVA), October 2022","DOI":"10.1007\/978-3-031-19992-9_1"},{"key":"5_CR77","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-53288-8_1","volume-title":"Computer Aided Verification","author":"HD Tran","year":"2020","unstructured":"Tran, H.D., et al.: NNV: the neural network verification tool for deep neural networks and learning-enabled cyber-physical systems. In: Lahiri, S.K., Wang, C. (eds.) Computer Aided Verification, pp. 3\u201317. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_1"},{"key":"5_CR78","doi-asserted-by":"crossref","unstructured":"Viswanadha, K., et al.: Addressing the IEEE AV test challenge with Scenic and VerifAI. In: IEEE International Conference on Artificial Intelligence Testing (AITest), pp. 136\u2013142. IEEE (2021)","DOI":"10.1109\/AITEST52744.2021.00034"},{"key":"5_CR79","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-030-88494-9_15","volume-title":"Runtime Verification","author":"K Viswanadha","year":"2021","unstructured":"Viswanadha, K., Kim, E., Indaheng, F., Fremont, D.J., Seshia, S.A.: Parallel and multi-objective falsification with Scenic and VerifAI. In: Feng, L., Fisman, D. (eds.) RV 2021. LNCS, vol. 12974, pp. 265\u2013276. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-88494-9_15"},{"key":"5_CR80","doi-asserted-by":"publisher","unstructured":"Vovk, V., Gammerman, A., Shafer, G.: Algorithmic Learning in a Random World. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/b106715","DOI":"10.1007\/b106715"},{"key":"5_CR81","unstructured":"Waite, T., Robey, A., Hamed, H., Pappas, G.J., Ivanov, R.: Data-driven modeling and verification of perception-based autonomous systems (2023)"},{"key":"5_CR82","doi-asserted-by":"publisher","unstructured":"Wang, Y., et al.: POLAR-express: efficient and precise formal reachability analysis of neural-network controlled systems. Trans. Comp.-Aided Des. Integr. Circuits Sys. 43(3), 994\u20131007 (2023). https:\/\/doi.org\/10.1109\/TCAD.2023.3331215","DOI":"10.1109\/TCAD.2023.3331215"},{"key":"5_CR83","unstructured":"Webots: http:\/\/www.cyberbotics.com, open-source Mobile Robot Simulation Software"},{"issue":"10","key":"5_CR84","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1145\/3448248","volume":"64","author":"JM Wing","year":"2021","unstructured":"Wing, J.M.: Trustworthy AI. Commun. ACM 64(10), 64\u201371 (2021)","journal-title":"Commun. ACM"},{"key":"5_CR85","doi-asserted-by":"publisher","unstructured":"Yalcinkaya, B., Torfah, H., Fremont, D.J., Seshia, S.A.: Compositional simulation-based analysis of AI-based autonomous systems for Markovian specifications. In: Katsaros, P., Nenzi, L. (eds.) Runtime Verification - 23rd International Conference, RV 2023, Thessaloniki, Greece, 3\u20136 October 2023, Proceedings. LNCS, vol. 14245, pp. 191\u2013212. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-44267-4_10","DOI":"10.1007\/978-3-031-44267-4_10"},{"key":"5_CR86","doi-asserted-by":"crossref","unstructured":"Yang, S., Pappas, G.J., Mangharam, R., Lindemann, L.: Safe perception-based control under stochastic sensor uncertainty using conformal prediction. In: 2023 62nd IEEE Conference on Decision and Control (CDC), pp. 6072\u20136078. IEEE (2023)","DOI":"10.1109\/CDC49753.2023.10384075"},{"key":"5_CR87","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-642-31424-7_27","volume-title":"Computer Aided Verification","author":"A Zutshi","year":"2012","unstructured":"Zutshi, A., Sankaranarayanan, S., Tiwari, A.: Timed relational abstractions for sampled data control systems. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 343\u2013361. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_27"}],"container-title":["Lecture Notes in Computer Science","Principles of Verification: Cycling the Probabilistic Landscape"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-75778-5_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,17]],"date-time":"2024-11-17T13:02:41Z","timestamp":1731848561000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-75778-5_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,18]]},"ISBN":["9783031757778","9783031757785"],"references-count":87,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-75778-5_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,11,18]]},"assertion":[{"value":"18 November 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}