{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,25]],"date-time":"2025-10-25T22:36:39Z","timestamp":1761431799283,"version":"build-2065373602"},"publisher-location":"Cham","reference-count":99,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783032087065"},{"type":"electronic","value":"9783032087072"}],"license":[{"start":{"date-parts":[[2025,10,26]],"date-time":"2025-10-26T00:00:00Z","timestamp":1761436800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,10,26]],"date-time":"2025-10-26T00:00:00Z","timestamp":1761436800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-08707-2_11","type":"book-chapter","created":{"date-parts":[[2025,10,25]],"date-time":"2025-10-25T22:33:48Z","timestamp":1761431628000},"page":"231-259","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Towards Unified Probabilistic Verification and\u00a0Validation of\u00a0Vision-Based Autonomy"],"prefix":"10.1007","author":[{"given":"Jordan","family":"Peper","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yan","family":"Miao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sayan","family":"Mitra","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ivan","family":"Ruchkin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,10,26]]},"reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"Aichernig, B.K., Tappler, M.: Probabilistic black-box reachability checking (extended version). Form. Methods Syst. Des. 54(3), 416\u2013448 (2019)","DOI":"10.1007\/s10703-019-00333-0"},{"key":"11_CR2","doi-asserted-by":"publisher","unstructured":"Alasmari, N., Calinescu, R., Paterson, C., Mirandola, R.: Quantitative verification with adaptive uncertainty reduction. J. Syst. Softw. 188, 111275 (2022). https:\/\/doi.org\/10.1016\/j.jss.2022.111275, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S016412122200036X","DOI":"10.1016\/j.jss.2022.111275"},{"key":"11_CR3","doi-asserted-by":"crossref","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)","DOI":"10.1145\/3622875"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"Badings, T., Cubuktepe, M., Jansen, N., Junges, S., Katoen, J.P., Topcu, U.: Scenario-based verification of uncertain parametric MDPs. Int. J. Softw. Tools Technol. Transf. 24(5), 803\u2013819 (2022)","DOI":"10.1007\/s10009-022-00673-z"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"Badings, T., Junges, S., Marandi, A., Topcu, U., Jansen, N.: Efficient sensitivity analysis for parametric robust Markov chains. In: 35th International Conference on Computer Aided Verification (2023)","DOI":"10.1007\/978-3-031-37709-9_4"},{"key":"11_CR6","doi-asserted-by":"publisher","unstructured":"Badithela, A., Wongpiromsarn, T., Murray, R.M.: Evaluation Metrics for Object Detection for Autonomous Systems (2022). https:\/\/doi.org\/10.48550\/arXiv.2210.10298, http:\/\/arxiv.org\/abs\/2210.10298, arXiv:2210.10298 [cs, eess]","DOI":"10.48550\/arXiv.2210.10298"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"Bakirtzis, G., Subrahmanian, E., Fleming, C.H.: Compositional thinking in cyberphysical systems theory. Computer 54(12), 50\u201359 (2021)","DOI":"10.1109\/MC.2021.3085532"},{"key":"11_CR8","doi-asserted-by":"publisher","unstructured":"Bensalem, S., Cheng, C.H., Huang, W., Huang, X., Wu, C., Zhao, X.: What, indeed, is an achievable provable guarantee for learning-enabled safety-critical systems. In: Steffen, B. (eds.) Bridging the Gap Between AI and Reality. AISoLA 2023. LNCS, vol. 14380, pp. 55\u201376. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-46002-9_4","DOI":"10.1007\/978-3-031-46002-9_4"},{"key":"11_CR9","doi-asserted-by":"crossref","unstructured":"Bharadwaj, S., Roux, S.L., Perez, G., Topcu, U.: Reduction Techniques for Model Checking and Learning in MDPs, pp. 4273\u20134279 (2017). https:\/\/www.ijcai.org\/proceedings\/2017\/597","DOI":"10.24963\/ijcai.2017\/597"},{"key":"11_CR10","doi-asserted-by":"publisher","unstructured":"Blundell, C., Giannakopoulou, D., P\u01ces\u01cereanu, C.S.: Assume-guarantee testing. SIGSOFT Softw. Eng. Notes 31(2), 1\u2013es (2005). https:\/\/doi.org\/10.1145\/1118537.1123060, https:\/\/dl.acm.org\/doi\/10.1145\/1118537.1123060","DOI":"10.1145\/1118537.1123060"},{"key":"11_CR11","doi-asserted-by":"publisher","unstructured":"Bojarski, M., et al.: End to End Learning for Self-Driving Cars (2016).https:\/\/doi.org\/10.48550\/arXiv.1604.07316, http:\/\/arxiv.org\/abs\/1604.07316, arXiv:1604.07316 [cs]","DOI":"10.48550\/arXiv.1604.07316"},{"key":"11_CR12","doi-asserted-by":"publisher","unstructured":"Brockman, G., et al.: OpenAI Gym (2016). https:\/\/doi.org\/10.48550\/arXiv.1606.01540, http:\/\/arxiv.org\/abs\/1606.01540, arXiv:1606.01540 [cs]","DOI":"10.48550\/arXiv.1606.01540"},{"key":"11_CR13","unstructured":"Calinescu, R., et al.: Controller Synthesis for Autonomous Systems With Deep-Learning Perception Components. IEEE Transactions on Software Engineering (2024). https:\/\/www.computer.org\/csdl\/journal\/ts\/2024\/06\/10496502\/1W28Vqz3hQc"},{"key":"11_CR14","unstructured":"Carpenter, T.J., Ivanov, R., Lee, I., Weimer, J.: ModelGuard: runtime validation of Lipschitz-continuous models. In: 7th IFAC Conference on Analysis and Design of Hybrid Systems (ADHS\u201921) (2021). arXiv: 2104.15006"},{"key":"11_CR15","doi-asserted-by":"publisher","unstructured":"Cauchois, M., Gupta, S., Ali, A., Duchi, J.C.: Robust validation: confident predictions even when distributions Shift. J. Am. Stat. Assoc. 1\u201366 (2024). https:\/\/doi.org\/10.1080\/01621459.2023.2298037","DOI":"10.1080\/01621459.2023.2298037"},{"key":"11_CR16","unstructured":"Chapman, M.P.: Risk-Sensitive Safety Analysis and Control for Trustworthy Autonomy. Ph.D., University of California, Berkeley, United States \u2013 California (2020). https:\/\/www.proquest.com\/docview\/2460739262\/abstract\/18015E97A18F4C45PQ\/1, iSBN: 9798678171221"},{"key":"11_CR17","doi-asserted-by":"publisher","unstructured":"Cleaveland, M., Lu, P., Sokolsky, O., Lee, I., Ruchkin, I.: Conservative Perception Models for Probabilistic Verification (2025). https:\/\/doi.org\/10.48550\/arXiv.2503.18077, http:\/\/arxiv.org\/abs\/2503.18077, arXiv:2503.18077 [cs] version: 2","DOI":"10.48550\/arXiv.2503.18077"},{"key":"11_CR18","doi-asserted-by":"publisher","unstructured":"Cleaveland, M., Ruchkin, I., Sokolsky, O., Lee, I.: Monotonic safety for scalable and data-efficient probabilistic safety analysis. In: ACM\/IEEE 13th International Conference on Cyber-Physical Systems (ICCPS), pp. 92\u2013103 (2022). https:\/\/doi.org\/10.1109\/ICCPS54341.2022.00015","DOI":"10.1109\/ICCPS54341.2022.00015"},{"key":"11_CR19","doi-asserted-by":"crossref","unstructured":"Cleaveland, M., Sokolsky, O., Lee, I., Ruchkin, I.: Conservative safety monitors of stochastic dynamical systems. In: Proceedings of the NASA Formal Methods Conference (May 2023)","DOI":"10.1007\/978-3-031-33170-1_9"},{"key":"11_CR20","doi-asserted-by":"publisher","unstructured":"Corso, A., Moss, R., Koren, M., Lee, R., Kochenderfer, M.: A survey of algorithms for black-box safety validation of cyber-physical systems. J. Artif. Intell. Rese. 72, 377\u2013428 (2022). https:\/\/doi.org\/10.1613\/jair.1.12716, https:\/\/dl.acm.org\/doi\/10.1613\/jair.1.12716","DOI":"10.1613\/jair.1.12716"},{"key":"11_CR21","doi-asserted-by":"publisher","unstructured":"Cubuktepe, M., Jansen, N., Junges, S., Katoen, J.P., Topcu, U.: Scenario-based verification of uncertain MDPs. In: In: Biere, A., Parker, D. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2020, LNCS, pp. 287\u2013305. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_16","DOI":"10.1007\/978-3-030-45190-5_16"},{"key":"11_CR22","doi-asserted-by":"publisher","unstructured":"C\u00e1mara, J.: HaiQ: synthesis of software design spaces with structural and probabilistic guarantees. In: Proceedings of the 8th International Conference on Formal Methods in Software Engineering, pp. 22\u201333. FormaliSE \u201920, Association for Computing Machinery, New York, NY, USA (2020). https:\/\/doi.org\/10.1145\/3372020.3391562","DOI":"10.1145\/3372020.3391562"},{"key":"11_CR23","doi-asserted-by":"publisher","unstructured":"D\u2019Innocenzo, A., Abate, A., Katoen, J.P.: Robust PCTL model checking. In: Proceedings of the 15th ACM international conference on Hybrid Systems: Computation and Control, pp. 275\u2013286. HSCC \u201912, Association for Computing Machinery, New York, NY, USA (2012). https:\/\/doi.org\/10.1145\/2185632.2185673","DOI":"10.1145\/2185632.2185673"},{"key":"11_CR24","doi-asserted-by":"publisher","unstructured":"Dong, Y., et al.: Reliability assessment and safety arguments for machine learning components in system assurance. ACM Trans. Embed. Comput. Syst. 22(3), 48:1\u201348:48 (2023).https:\/\/doi.org\/10.1145\/3570918, https:\/\/dl.acm.org\/doi\/10.1145\/3570918","DOI":"10.1145\/3570918"},{"key":"11_CR25","doi-asserted-by":"publisher","unstructured":"Dong, Y., Huang, J., Ai, J.: Visual perception-based target aircraft movement prediction for autonomous air combat. J. Aircraft 52(2), 538\u2013552 (2015). https:\/\/doi.org\/10.2514\/1.C032764, https:\/\/arc.aiaa.org\/doi\/10.2514\/1.C032764, publisher: American Institute of Aeronautics and Astronautics","DOI":"10.2514\/1.C032764"},{"key":"11_CR26","doi-asserted-by":"crossref","unstructured":"Dong, Y., Tao, J., Zhang, Y., Lin, W., Ai, J.: Deep learning in aircraft design, dynamics, and control: review and prospects. IEEE Trans. Aerosp. Electron. Syst. 57(4), 2346\u20132368 (2021)","DOI":"10.1109\/TAES.2021.3056086"},{"key":"11_CR27","doi-asserted-by":"crossref","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)","DOI":"10.1007\/s10817-018-09509-5"},{"key":"11_CR28","unstructured":"Dreossi, T., et al.: VERIFAI: A Toolkit for the Design and Analysis of Artificial Intelligence-Based Systems. arXiv:1902.04245 [cs] (2019). http:\/\/arxiv.org\/abs\/1902.04245, arXiv: 1902.04245"},{"key":"11_CR29","doi-asserted-by":"publisher","unstructured":"Dutta, S., et al.: Distributionally Robust Statistical Verification with Imprecise Neural Networks. In: Proceedings of the HSCC 2025. Springer (2025). https:\/\/doi.org\/10.48550\/arXiv.2308.14815","DOI":"10.48550\/arXiv.2308.14815"},{"issue":"4","key":"11_CR30","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1007\/s10009-015-0383-0","volume":"17","author":"P D\u2019Argenio","year":"2015","unstructured":"D\u2019Argenio, P., Legay, A., Sedwards, S., Traonouez, L.M.: Smart sampling for lightweight verification of markov decision processes. Int. J. Softw. Tools Technol. Transf. 17(4), 469\u2013484 (2015)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"11_CR31","doi-asserted-by":"crossref","unstructured":"Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications for continuous-time signals. Theor. Comput. Sci. 410(42), 4262\u20134291 (2009)","DOI":"10.1016\/j.tcs.2009.06.021"},{"key":"11_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1007\/978-3-642-24372-1_40","volume-title":"Automated Technology for Verification and Analysis","author":"L Feng","year":"2011","unstructured":"Feng, L., Han, T., Kwiatkowska, M., Parker, D.: Learning-based compositional verification for synchronous probabilistic systems. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 511\u2013521. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24372-1_40"},{"key":"11_CR33","unstructured":"Filos, A., Tigkas, P., Mcallister, R., Rhinehart, N., Levine, S., Gal, Y.: Can autonomous vehicles identify, recover from, and adapt to distribution shifts? In: Proceedings of the 37th International Conference on Machine Learning, pp. 3145\u20133153. PMLR (2020). https:\/\/proceedings.mlr.press\/v119\/filos20a.html, iSSN: 2640-3498"},{"key":"11_CR34","doi-asserted-by":"crossref","unstructured":"Fleiss, J.L., Levin, B., Paik, M.C.: Statistical Methods for Rates & Proportions, 3rd edn. Wiley-Interscience, Hoboken, N.J. (2003)","DOI":"10.1002\/0471445428"},{"key":"11_CR35","doi-asserted-by":"publisher","unstructured":"Frehse, G., Han, Z., Krogh, B.: Assume-guarantee reasoning for hybrid I\/O-automata by over-approximation of continuous interaction. In: Proceedings of the 43rd IEEE Conference on Decision and Control (CDC) (IEEE Cat. No. 04CH37601), vol.\u00a01, pp. 479\u2013484 (2004). https:\/\/doi.org\/10.1109\/CDC.2004.1428676","DOI":"10.1109\/CDC.2004.1428676"},{"key":"11_CR36","doi-asserted-by":"crossref","unstructured":"Frenkel, H., Grumberg, O., P\u0103s\u0103reanu, C.S., Sheinvald, S.: Assume, guarantee or repair: a regular framework for non regular properties. Int. J. Softw. Tools Technol. Transf. 24(5), 667\u2013689 (2022)","DOI":"10.1007\/s10009-022-00669-9"},{"key":"11_CR37","doi-asserted-by":"publisher","unstructured":"Fu, J., Topcu, U.: Probably Approximately Correct MDP Learning and Control With Temporal Logic Constraints. Robotics: Science and Systems X (2014). https:\/\/doi.org\/10.15607\/RSS.2014.X.039, http:\/\/www.roboticsproceedings.org\/rss10\/p39.pdf, conference Name: Robotics: Science and Systems 2014 ISBN: 9780992374709 Publisher: Robotics: Science and Systems Foundation","DOI":"10.15607\/RSS.2014.X.039"},{"key":"11_CR38","doi-asserted-by":"publisher","unstructured":"Graf, S., Passerone, R., Quinton, S.: Contract-based reasoning for component systems with rich interactions. In: Sangiovanni-Vincentelli, A., Zeng, H., Di Natale, M., Marwedel, P. (eds.) Embedded Systems Development. Embedded Systems, LNCS, vol. 20, pp. 139\u2013154. Springer, New York (2014). https:\/\/doi.org\/10.1007\/978-1-4614-3879-3_8","DOI":"10.1007\/978-1-4614-3879-3_8"},{"key":"11_CR39","unstructured":"Gupta, C., Podkopaev, A., Ramdas, A.: Distribution-free binary classification: prediction sets, confidence intervals and calibration. arXiv:2006.10564 [cs, math, stat] (2022). http:\/\/arxiv.org\/abs\/2006.10564, arXiv:2006.10564"},{"key":"11_CR40","doi-asserted-by":"publisher","unstructured":"Hensel, C., Junges, S., Katoen, J.P., Quatmann, T., Volk, M.: The Probabilistic Model Checker Storm (2020). https:\/\/doi.org\/10.48550\/arXiv.2002.07080, http:\/\/arxiv.org\/abs\/2002.07080, arXiv:2002.07080 [cs]","DOI":"10.48550\/arXiv.2002.07080"},{"key":"11_CR41","doi-asserted-by":"publisher","unstructured":"Holtzen, S., Junges, S., Vazquez-Chanlatte, M., Millstein, T., Seshia, S.A., Van den Broeck, G.: Model checking finite-horizon Markov chains with probabilistic inference. In: Silva, A., Leino, K.R.M. (eds.) Computer Aided Verification. CAV 2021. LNCS, vol. 12760, pp. 577\u2013601. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_27","DOI":"10.1007\/978-3-030-81688-9_27"},{"key":"11_CR42","unstructured":"Holtzen, S., Millstein, T., Broeck, G.V.D.: Probabilistic Program Abstractions. arXiv:1705.09970 [cs] (2017),.http:\/\/arxiv.org\/abs\/1705.09970, arXiv: 1705.09970"},{"key":"11_CR43","unstructured":"Howard, R.A.: Dynamic Probabilistic Systems, Volume II: Semi-Markov and Decision Processes, 1 edn. Dover Publications, New York (June 2007)"},{"key":"11_CR44","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":"11_CR45","doi-asserted-by":"publisher","unstructured":"Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety verification of deep neural networks. In: Majumdar, R., Kun\u010dak, V. (eds.) Computer Aided Verification. CAV 2017. LNCS, vol. 10426, pp. 3\u201329. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_1","DOI":"10.1007\/978-3-319-63387-9_1"},{"key":"11_CR46","doi-asserted-by":"publisher","unstructured":"Incer, I., Benveniste, A., Sangiovanni-Vincentelli, A., Seshia, S.A.: Hypercontracts. In: NASA Formal Methods: 14th International Symposium, NFM 2022, Pasadena, CA, USA, 24\u201327 May 2022, Proceedings, pp. 674\u2013692. Springer, Berlin, Heidelberg (2022). https:\/\/doi.org\/10.1007\/978-3-031-06773-0_36","DOI":"10.1007\/978-3-031-06773-0_36"},{"key":"11_CR47","doi-asserted-by":"publisher","unstructured":"Ivanov, R., Carpenter, T.J., Weimer, J., Alur, R., Pappas, G.J., Lee, I.: Case study: verifying the safety of an autonomous racing car with a neural network controller. In: Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control, pp.\u00a01\u20137. HSCC \u201920, Association for Computing Machinery, New York, NY, USA (2020). https:\/\/doi.org\/10.1145\/3365365.3382216, https:\/\/dl.acm.org\/doi\/10.1145\/3365365.3382216","DOI":"10.1145\/3365365.3382216"},{"key":"11_CR48","unstructured":"Jackson, J., Laurenti, L., Frew, E., Lahijanian, M.: Formal Verification of Unknown Dynamical Systems via Gaussian Process Regression (2021). https:\/\/www.semanticscholar.org\/paper\/Formal-Verification-of-Unknown-Dynamical-Systems-Jackson-Laurenti\/8093250cc2b5876880717afc806ee7f2a35fd1ba"},{"key":"11_CR49","doi-asserted-by":"publisher","unstructured":"Katoen, J.P.: The probabilistic model checking landscape. In: Proceedings of the 31st Annual ACM\/IEEE Symposium on Logic in Computer Science, pp. 31\u201345. LICS \u201916, Association for Computing Machinery, New York, NY, USA (2016). https:\/\/doi.org\/10.1145\/2933575.2934574","DOI":"10.1145\/2933575.2934574"},{"key":"11_CR50","doi-asserted-by":"crossref","unstructured":"Kerbl, B., Kopanas, G., Leimk\u00fchler, T., Drettakis, G.: 3D gaussian splatting for real-time radiance field rendering. ACM Trans. Graph. 42(4) (2023). https:\/\/repo-sam.inria.fr\/fungraph\/3d-gaussian-splatting\/","DOI":"10.1145\/3592433"},{"key":"11_CR51","doi-asserted-by":"publisher","unstructured":"Komuravelli, A., Pasareanu, C.S., Clarke, E.M.: Assume-Guarantee Abstraction Refinement for Probabilistic Systems. arXiv:1207.5086 [cs] $$\\textbf{7358}$$, 310\u2013326 (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_25, http:\/\/arxiv.org\/abs\/1207.5086, arXiv: 1207.5086","DOI":"10.1007\/978-3-642-31424-7_25"},{"key":"11_CR52","unstructured":"Kurakin, A., Goodfellow, I.J., Bengio, S.: Adversarial examples in the physical world. In: Proceedings of the ICLR 2016 (2017). https:\/\/openreview.net\/forum?id=HJGU3Rodl"},{"key":"11_CR53","doi-asserted-by":"publisher","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Stochastic model checking. In: Bernardo, M., Hillston, J. (eds.) Formal Methods for Performance Evaluation. SFM 2007. LNCS, vol. 4486, pp. 220\u2013270. Springer, Berlin, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-72522-0_6","DOI":"10.1007\/978-3-540-72522-0_6"},{"key":"11_CR54","doi-asserted-by":"publisher","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","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"11_CR55","doi-asserted-by":"publisher","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic model checking and autonomy. Annu. Rev. Control Robot. Auton. Syst. 5(1), 385\u2013410 (2022). https:\/\/doi.org\/10.1146\/annurev-control-042820-010947, https:\/\/doi.org\/10.1146\/annurev-control-042820-010947, _eprint","DOI":"10.1146\/annurev-control-042820-010947"},{"key":"11_CR56","doi-asserted-by":"publisher","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Qu, H.: Assume-guarantee verification for probabilistic systems. In: Esparza, J., Majumdar, R. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2010. LNCS, vol. 6015, pp. 23\u201337. Springer, Berlin, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-12002-2_3","DOI":"10.1007\/978-3-642-12002-2_3"},{"key":"11_CR57","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1016\/j.ic.2013.10.001","volume":"232","author":"M Kwiatkowska","year":"2013","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Qu, H.: Compositional probabilistic verification through multi-objective model checking. Inf. Comput. 232, 38\u201365 (2013)","journal-title":"Inf. Comput."},{"key":"11_CR58","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Zhang, X.: When to trust AI: advances and challenges for certification of neural networks. Ann. Comput. Sci. Inf. Syst. 35, 25\u201337 (2023). https:\/\/annals-csis.org\/Volume_35\/drp\/2324.html, iSSN: 2300-5963","DOI":"10.15439\/2023F2324"},{"key":"11_CR59","doi-asserted-by":"publisher","unstructured":"Legay, A., Sedwards, S., Traonouez, L.M.: Scalable verification of markov decision processes. In: Canal, C., Idani, A. (eds.) Software Engineering and Formal Methods. SEFM 2014. LNCS, vol. 8938, pp. 350\u2013362. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-15201-1_23","DOI":"10.1007\/978-3-319-15201-1_23"},{"key":"11_CR60","doi-asserted-by":"publisher","unstructured":"Li, J., Nuzzo, P., Sangiovanni-Vincentelli, A., Xi, Y., Li, D.: Stochastic contracts for cyber-physical system design under probabilistic requirements. In: Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design, pp. 5\u201314. MEMOCODE \u201917, Association for Computing Machinery, New York, NY, USA (2017). https:\/\/doi.org\/10.1145\/3127041.3127045","DOI":"10.1145\/3127041.3127045"},{"key":"11_CR61","unstructured":"Li, Y., Ji, C., Anchalia, J., Mitra, S.: Lyapunov perception contracts. In: In Proceedings of Learning for Decision and Control (L4DC) (2025)"},{"key":"11_CR62","doi-asserted-by":"publisher","unstructured":"Liebenwein, L., et al.: Compositional and contract-based verification for autonomous driving on road networks. In: Amato, N., Hager, G., Thomas, S., Torres-Torriti, M. (eds.) Robotics Research. Springer Proceedings in Advanced Robotics, vol. 10, pp. 163\u2013181. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-28619-4_18","DOI":"10.1007\/978-3-030-28619-4_18"},{"key":"11_CR63","unstructured":"Lomuscio, A., Pirovano, E.: A Counter abstraction technique for the verification of probabilistic swarm systems. In: Proceedings of the 18th International Conference on Autonomous Agents and MultiAgent Systems, pp. 161\u2013169. AAMAS \u201919, International Foundation for Autonomous Agents and Multiagent Systems, Richland, SC (May 2019)"},{"key":"11_CR64","doi-asserted-by":"publisher","unstructured":"Majumdar, A., Pavone, M.: How should a robot assess risk? Towards an axiomatic theory of risk in robotics. In: Amato, N., Hager, G., Thomas, S., Torres-Torriti, M. (eds.) Robotics Research. Springer Proceedings in Advanced Robotics, LNCS, vol. 10, pp. 75\u201384. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-28619-4_10","DOI":"10.1007\/978-3-030-28619-4_10"},{"key":"11_CR65","doi-asserted-by":"crossref","unstructured":"Mallik, K., Schmuck, A.K., Soudjani, S., Majumdar, R.: Compositional synthesis of finite-state abstractions. IEEE Trans. Autom. Control 64(6), 2629\u20132636 (2018). publisher: IEEE","DOI":"10.1109\/TAC.2018.2869740"},{"key":"11_CR66","unstructured":"Miao, Y., Shen, W., Cui, H., Mitra, S.: Falconwing: an open-source platform for ultra-light fixed-wing aircraft research (2025). https:\/\/arxiv.org\/abs\/2505.01383"},{"key":"11_CR67","unstructured":"Miao, Y., Shen, W., Mitra, S.: Zero-shot sim-to-real visual quadrotor control with hard constraints. In: IEEE\/RSJ International Conference on Intelligent Robots and Systems. Hangzhou, China (October 2025)"},{"key":"11_CR68","doi-asserted-by":"crossref","unstructured":"Mildenhall, B., Srinivasan, P.P., Tancik, M., Barron, J.T., Ramamoorthi, R., Ng, R.: Nerf: representing scenes as neural radiance fields for view synthesis. Commun. ACM 65(1), 99\u2013106 (2021)","DOI":"10.1145\/3503250"},{"key":"11_CR69","doi-asserted-by":"publisher","unstructured":"Mitra, S., et al.: Formal verification techniques for vision-based autonomous systems \u2013 a survey. In: Jansen, N., et al. (eds.) Principles of Verification: Cycling the Probabilistic Landscape. LNCS, vol. 15262, pp. 89\u2013108. Springer, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-75778-5_5","DOI":"10.1007\/978-3-031-75778-5_5"},{"key":"11_CR70","doi-asserted-by":"publisher","unstructured":"Moss, R.J., Kochenderfer, M.J., Gariel, M., Dubois, A.: Bayesian safety validation for black-box systems. In: Conference proceedings of the 2023 AIAA AVIATION Forum (May 2023). https:\/\/doi.org\/10.48550\/arXiv.2305.02449, http:\/\/arxiv.org\/abs\/2305.02449, arXiv:2305.02449 [cs, stat]","DOI":"10.48550\/arXiv.2305.02449"},{"key":"11_CR71","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":"11_CR72","doi-asserted-by":"crossref","unstructured":"Newcombe, R.G.: Two-sided confidence intervals for the single proportion: comparison of seven methods. Stat. Med. 17(8), 857\u2013872 (1998)","DOI":"10.1002\/(SICI)1097-0258(19980430)17:8<857::AID-SIM777>3.0.CO;2-E"},{"key":"11_CR73","doi-asserted-by":"publisher","unstructured":"Nuzzo, P.: From electronic design automation to cyber-physical system design automation: a tale of platforms and contracts. In: Proceedings of the 2019 International Symposium on Physical Design, pp. 117\u2013121. ISPD \u201919, Association for Computing Machinery, San Francisco, CA, USA (2019). https:\/\/doi.org\/10.1145\/3299902.3311070","DOI":"10.1145\/3299902.3311070"},{"key":"11_CR74","doi-asserted-by":"publisher","unstructured":"Nuzzo, P., Li, J., Sangiovanni-Vincentelli, A.L., Xi, Y., Li, D.: Stochastic assume-guarantee contracts for cyber-physical system design. ACM Trans. Embed. Comput. Syst. 18(1), 2:1\u20132:26 (2019). https:\/\/doi.org\/10.1145\/3243216","DOI":"10.1145\/3243216"},{"key":"11_CR75","doi-asserted-by":"publisher","unstructured":"Peper, J., Miao, Y., Mitra, S., Ruchkin, I.: Towards Unified Probabilistic Verification and Validation of Vision-Based Autonomy (2025). https:\/\/doi.org\/10.48550\/arXiv.2508.14181, http:\/\/arxiv.org\/abs\/2508.14181, arXiv:2508.14181 [eess]","DOI":"10.48550\/arXiv.2508.14181"},{"key":"11_CR76","doi-asserted-by":"publisher","unstructured":"Puggelli, A., Li, W., Sangiovanni-Vincentelli, A.L., Seshia, S.A.: Polynomial-time verification of PCTL properties of MDPs with convex uncertainties. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 527\u2013542. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_35","DOI":"10.1007\/978-3-642-39799-8_35"},{"key":"11_CR77","doi-asserted-by":"publisher","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. CAV 2023. LNCS, vol. 13964, pp. 289\u2013303. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-37706-8_15","DOI":"10.1007\/978-3-031-37706-8_15"},{"key":"11_CR78","doi-asserted-by":"publisher","unstructured":"Ruchkin, I., Sokolsky, O., Weimer, J., Hedaoo, T., Lee, I.: Compositional probabilistic analysis of temporal properties over stochastic detectors. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. 39(11), 3288\u20133299 (2020). https:\/\/doi.org\/10.1109\/TCAD.2020.3012643","DOI":"10.1109\/TCAD.2020.3012643"},{"key":"11_CR79","unstructured":"Ruchkin, I.: Integration of Modeling Methods for Cyber-Physical Systems. PhD Thesis, Carnegie Mellon University (2019). https:\/\/doi.org\/10.1184\/R1\/7970222.v1"},{"key":"11_CR80","doi-asserted-by":"publisher","unstructured":"Ruchkin, I., et al.: Confidence composition for monitors of verification assumptions. In: ACM\/IEEE 13th International Conference on Cyber-Physical Systems (ICCPS), pp. 1\u201312 (2022). https:\/\/doi.org\/10.1109\/ICCPS54341.2022.00007","DOI":"10.1109\/ICCPS54341.2022.00007"},{"key":"11_CR81","doi-asserted-by":"crossref","unstructured":"Ruchkin, I., de\u00a0Niz, D., Chaki, S., Garlan, D.: ACTIVE: a tool for integrating analysis contracts. In: 5th Analytic Virtual Integration of Cyber-Physical Systems Workshop. Rome, Italy (2014)","DOI":"10.21236\/ADA610323"},{"key":"11_CR82","doi-asserted-by":"publisher","unstructured":"Ruchkin, I., de\u00a0Niz, D., Chaki, S., Garlan, D.: Contract-based integration of cyber-physical analyses. In: Proceedings of the International Conference on Embedded Software (EMSOFT). ACM, New York, NY, USA (2014). https:\/\/doi.org\/10.1145\/2656045.2656052","DOI":"10.1145\/2656045.2656052"},{"key":"11_CR83","doi-asserted-by":"publisher","unstructured":"Rushby, J.: Composing safe systems. In: Arbab, F., \u00d6lveczky, P.C. (eds.) Formal Aspects of Component Software. FACS 2011. LNCS, vol. 7253, pp. 3\u201311. Springer, Berlin, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-35743-5_2","DOI":"10.1007\/978-3-642-35743-5_2"},{"key":"11_CR84","doi-asserted-by":"publisher","unstructured":"Sangiovanni-Vincentelli, A., Damm, W., Passerone, R.: Taming Dr. Frankenstein: contract-based design for cyber-physical systems. Eur. J. Control 18(3), 217\u2013238 (2012). https:\/\/doi.org\/10.3166\/ejc.18.217-238","DOI":"10.3166\/ejc.18.217-238"},{"key":"11_CR85","doi-asserted-by":"publisher","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. NFM 2022. LNCS, vol. 13260, pp. 213\u2013230. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-06773-0_11","DOI":"10.1007\/978-3-031-06773-0_11"},{"key":"11_CR86","doi-asserted-by":"publisher","unstructured":"Shvets, A.A., Rakhlin, A., Kalinin, A.A., Iglovikov, V.I.: Automatic instrument segmentation in robot-assisted surgery using deep learning. In: 2018 17th IEEE International Conference on Machine Learning and Applications (ICMLA), pp. 624\u2013628 (2018). https:\/\/doi.org\/10.1109\/ICMLA.2018.00100, https:\/\/ieeexplore.ieee.org\/document\/8614125","DOI":"10.1109\/ICMLA.2018.00100"},{"key":"11_CR87","doi-asserted-by":"publisher","unstructured":"Sun, D., Yang, B.C., Mitra, S.: Learning-based inverse perception contracts and applications. In: 2024 IEEE International Conference on Robotics and Automation (ICRA), pp. 11612\u201311618 (2024). https:\/\/doi.org\/10.1109\/ICRA57147.2024.10610329","DOI":"10.1109\/ICRA57147.2024.10610329"},{"key":"11_CR88","unstructured":"Szegedy, C., et al.: Intriguing properties of neural networks. In: International Conference on Learning Representations (2014)"},{"key":"11_CR89","unstructured":"Termine, A., Antonucci, A., Facchini, A., Primiero, G.: Robust model checking with imprecise markov reward models. In: Proceedings of the Twelveth International Symposium on Imprecise Probability: Theories and Applications, pp. 299\u2013309. PMLR (2021). https:\/\/proceedings.mlr.press\/v147\/termine21a.html, iSSN: 2640-3498"},{"key":"11_CR90","unstructured":"Troffaes, M.C.M., Skulj, D.: Model checking for imprecise Markov chains. In: Proceedings of the Eighth International Symposium on Imprecise Probability: Theories and Applications, pp. 337\u2013344. Society for Imprecise Probability: Theories and Applications (SIPTA), Compiegne, France (2013). http:\/\/www.sipta.org\/isipta13\/index.php?id=paper&paper=034.html, conference Name: ISIPTA\u201913: Proceedings of the Eighth International Symposium on Imprecise Probability: Theories and Applications Meeting Name: ISIPTA\u201913: Proceedings of the Eighth International Symposium on Imprecise Probability: Theories and Applications"},{"key":"11_CR91","unstructured":"Vazquez-Chanlatte, M., Rabe, M.N., Seshia, S.A.: A Model Counter\u2019s Guide to Probabilistic Systems. arXiv:1903.09354 [cs] (2019). http:\/\/arxiv.org\/abs\/1903.09354, arXiv: 1903.09354"},{"key":"11_CR92","doi-asserted-by":"publisher","unstructured":"Waite, T., Geng, Y., Turnquist, T., Ruchkin, I., Ivanov, R.: State-Dependent Conformal Perception Bounds for Neuro-Symbolic Verification of Autonomous Systems (2025). https:\/\/doi.org\/10.48550\/arXiv.2502.21308, http:\/\/arxiv.org\/abs\/2502.21308, arXiv:2502.21308 [eess]","DOI":"10.48550\/arXiv.2502.21308"},{"key":"11_CR93","doi-asserted-by":"publisher","unstructured":"Wang, Z., Huang, C., Wang, Y., Hobbs, C., Chakraborty, S., Zhu, Q.: Bounding perception neural network uncertainty for safe control of autonomous systems. In: 2021 Design, Automation & Test in Europe Conference & Exhibition (DATE), pp. 1745\u20131750 (2021). https:\/\/doi.org\/10.23919\/DATE51398.2021.9474204, iSSN: 1558-1101","DOI":"10.23919\/DATE51398.2021.9474204"},{"key":"11_CR94","doi-asserted-by":"publisher","unstructured":"Wolff, E.M., Topcu, U., Murray, R.M.: Robust control of uncertain Markov decision processes with temporal logic specifications. In: 2012 IEEE 51st IEEE Conference on Decision and Control (CDC), pp. 3372\u20133379 (2012). https:\/\/doi.org\/10.1109\/CDC.2012.6426174, iSSN: 0743-1546","DOI":"10.1109\/CDC.2012.6426174"},{"key":"11_CR95","doi-asserted-by":"publisher","unstructured":"Wu, H., et al.: Toward certified robustness against real-world distribution shifts. 2023 IEEE Conference on Secure and Trustworthy Machine Learning (SaTML), pp. 537\u2013553 (2023). https:\/\/doi.org\/10.1109\/SaTML54575.2023.00042, https:\/\/ieeexplore.ieee.org\/document\/10136136\/, conference Name: 2023 IEEE Conference on Secure and Trustworthy Machine Learning (SaTML) ISBN: 9781665462990 Place: Raleigh, NC, USA Publisher: IEEE","DOI":"10.1109\/SaTML54575.2023.00042"},{"key":"11_CR96","unstructured":"Xie, X., Song, J., Zhou, Z., Zhang, F., Ma, L.: Mosaic: Model-based Safety Analysis Framework for AI-enabled Cyber-Physical Systems (May 2023). http:\/\/arxiv.org\/abs\/2305.03882, arXiv:2305.03882 [cs]"},{"key":"11_CR97","doi-asserted-by":"crossref","unstructured":"Xie, Z., Liu, Z., Peng, Z., Wu, W., Zhou, B.: Vid2sim: realistic and interactive simulation from video for urban navigation. CVPR (2025)","DOI":"10.1109\/CVPR52734.2025.00155"},{"key":"11_CR98","doi-asserted-by":"crossref","unstructured":"Yang, S., et al.: Novel demonstration generation with gaussian splatting enables robust one-shot manipulation. arXiv preprint arXiv:2504.13175 (2025)","DOI":"10.15607\/RSS.2025.XXI.146"},{"key":"11_CR99","doi-asserted-by":"crossref","unstructured":"Zhao, X., Gerasimou, S., Calinescu, R., Imrie, C., Robu, V., Flynn, D.: Bayesian learning for the robust verification of autonomous robots. Commun. Eng. 3(1), 1\u201314 (2024)","DOI":"10.1038\/s44172-024-00162-y"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-08707-2_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,25]],"date-time":"2025-10-25T22:33:58Z","timestamp":1761431638000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-08707-2_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,26]]},"ISBN":["9783032087065","9783032087072"],"references-count":99,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-08707-2_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025,10,26]]},"assertion":[{"value":"26 October 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ATVA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Automated Technology for Verification and Analysis","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Bengaluru","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"India","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":"27 October 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 October 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"atva2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/atva-2025","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}