{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,19]],"date-time":"2026-08-19T10:30:30Z","timestamp":1787135430519,"version":"3.56.0"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031999901","type":"print"},{"value":"9783031999918","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:00:00Z","timestamp":1761609600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:00:00Z","timestamp":1761609600000},"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-031-99991-8_1","type":"book-chapter","created":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T05:36:15Z","timestamp":1761543375000},"page":"3-28","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Scenario-Based Compositional Verification of\u00a0Autonomous Systems with\u00a0Neural Perception"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3716-516X","authenticated-orcid":false,"given":"Christopher","family":"Watson","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1733-7083","authenticated-orcid":false,"given":"Rajeev","family":"Alur","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1242-7701","authenticated-orcid":false,"given":"Divya","family":"Gopinath","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6267-6995","authenticated-orcid":false,"given":"Ravi","family":"Mangal","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5579-6961","authenticated-orcid":false,"given":"Corina S.","family":"P\u0103s\u0103reanu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,10,28]]},"reference":[{"key":"1_CR1","doi-asserted-by":"crossref","unstructured":"Arjomand\u00a0Bigdeli, 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":"1_CR2","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":"1_CR3","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":"1_CR4","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":"1_CR5","doi-asserted-by":"crossref","unstructured":"Cai, F., Fan, C., Bak, S.: Scalable surrogate verification of image-based neural network control systems using composition and unrolling (2024)","DOI":"10.1609\/aaai.v39i1.31976"},{"key":"1_CR6","unstructured":"Calinescu, R., Imrie, C., Mangal, R., Pasareanu, C.S., Santana, M.A., V\u00e1zquez, G.: Discrete-event controller synthesis for autonomous systems with deep-learning perception components. CoRR arxiv:2202.03360 (2022)"},{"key":"1_CR7","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":"1_CR8","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":"1_CR9","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS\u201908\/ETAPS\u201908, pp. 337\u2013340. Springer-Verlag, Heidelberg (2008). http:\/\/dl.acm.org\/citation.cfm?id=1792734.1792766","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"1_CR10","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) (2020)","DOI":"10.1007\/978-3-030-53288-8_6"},{"key":"1_CR11","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) (2020)","DOI":"10.1109\/ITSC45102.2020.9294368"},{"key":"1_CR12","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 arxiv:1910.07738 (2019)","DOI":"10.1002\/rob.21918"},{"key":"1_CR13","unstructured":"Gurobi Optimization, LLC: Gurobi Optimizer Reference Manual (2024). https:\/\/www.gurobi.com"},{"key":"1_CR14","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":"1_CR15","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"},{"issue":"4","key":"1_CR16","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":"1_CR17","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":"1_CR18","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":"1_CR19","doi-asserted-by":"publisher","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":"1_CR20","doi-asserted-by":"publisher","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. 20(5s) (2021). https:\/\/doi.org\/10.1145\/3477023","DOI":"10.1145\/3477023"},{"key":"1_CR21","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, Lecture Notes in Computer Science, pp. 104\u2013121. Springer, Heidelberg (2021). https:\/\/doi.org\/10.1007\/978-3-030-95561-8_7","DOI":"10.1007\/978-3-030-95561-8_7"},{"issue":"9","key":"1_CR22","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. Aeros. Inf. Syst. 19(9), 574\u2013584 (2022)","journal-title":"J. Aeros. Inf. Syst."},{"key":"1_CR23","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":"1_CR24","doi-asserted-by":"crossref","unstructured":"Li, J., Nuzzo, P., Sangiovanni-Vincentelli, A., Xi, Y., Li, D.: Stochastic assume-guarantee contracts for cyber-physical system design under probabilistic requirements (2017). https:\/\/arxiv.org\/abs\/1705.09316","DOI":"10.1145\/3127041.3127045"},{"key":"1_CR25","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":"1_CR26","doi-asserted-by":"publisher","unstructured":"Morgan, C.,McIver, A., Seidel, K.: Probabilistic predicate transformers. ACM Trans. Program. Lang. Syst. 18(3), 325\u2013353 (1996). https:\/\/doi.org\/10.1145\/229542.229547","DOI":"10.1145\/229542.229547"},{"key":"1_CR27","unstructured":"O\u2019Kelly, M., Zheng, H., Karthik, D., Mangharam, R.: F1tenth: an open-source evaluation environment for continuous control and reinforcement learning. In: Escalante, H.J., Hadsell, R. (eds.) Proceedings of the NeurIPS 2019 Competition and Demonstration Track. Proceedings of Machine Learning Research, vol.\u00a0123, pp. 77\u201389. PMLR (2020). https:\/\/proceedings.mlr.press\/v123\/o-kelly20a.html"},{"key":"1_CR28","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":"1_CR29","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. Lecture Notes in Computer Science, vol. 14245, pp. 3\u201322. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-44267-4_1","DOI":"10.1007\/978-3-031-44267-4_1"},{"key":"1_CR30","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":"1_CR31","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":"1_CR32","unstructured":"Tabernik, D., Skocaj, D.: Deep learning for large-scale traffic-sign detection and recognition. CoRR arxiv:1904.00649 (2019)"},{"key":"1_CR33","unstructured":"Waite, T., Robey, A., Hamed, H., Pappas, G.J., Ivanov, R.: Data-driven modeling and verification of perception-based autonomous systems (2023)"},{"key":"1_CR34","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/978-3-031-37709-9_3","volume-title":"Computer Aided Verification","author":"K Watanabe","year":"2023","unstructured":"Watanabe, K., Eberhart, C., Asada, K., Hasuo, I.: Compositional probabilistic model checking with string diagrams of mdps. In: Enea, C., Lal, A. (eds.) Computer Aided Verification, pp. 40\u201361. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-37709-9_3"},{"key":"1_CR35","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/978-3-031-44267-4_10","volume-title":"Runtime Verification","author":"B Yalcinkaya","year":"2023","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, pp. 191\u2013212. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-44267-4_10"}],"container-title":["Lecture Notes in Computer Science","AI Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-99991-8_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,19]],"date-time":"2026-08-19T10:14:18Z","timestamp":1787134458000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-99991-8_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,28]]},"ISBN":["9783031999901","9783031999918"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-99991-8_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,28]]},"assertion":[{"value":"28 October 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SAIV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on AI Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Zagreb","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Croatia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"saiv2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.aiverification.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}