{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,11]],"date-time":"2025-11-11T12:15:06Z","timestamp":1762863306951,"version":"3.44.0"},"publisher-location":"Cham","reference-count":93,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031986789"},{"type":"electronic","value":"9783031986796"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T00:00:00Z","timestamp":1753142400000},"content-version":"vor","delay-in-days":202,"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>\n          <jats:p>This paper presents StarV, a new tool for verifying deep neural networks (DNNs) and learning-enabled Cyber-Physical Systems (Le-CPS) using the well-known star reachability. Distinguished from existing star-based verification tools such as NNV and NNENUM and others, StarV not only offers qualitative verification techniques using Star and ImageStar reachability analysis but is also the first tool to propose using ProbStar reachability for quantitative verification of DNNs with piecewise linear activation functions and Le-CPS. Notably, it introduces a novel ProbStar Temporal Logic formalism and associated algorithms, enabling the quantitative verification of DNNs and Le-CPS\u2019s temporal behaviors. Additionally, StarV presents a novel SparseImageStar set representation and associated reachability algorithm that allows users to verify deep convolutional neural networks and semantic segmentation networks with more memory efficiency. StarV is evaluated in comparison with state-of-the-art in many challenging benchmarks. The experiments show that StarV outperforms existing tools in many aspects, such as timing performance, scalability, and memory consumption.<\/jats:p>","DOI":"10.1007\/978-3-031-98679-6_17","type":"book-chapter","created":{"date-parts":[[2025,7,21]],"date-time":"2025-07-21T09:21:20Z","timestamp":1753089680000},"page":"376-394","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["StarV: A Qualitative and\u00a0Quantitative Verification Tool for\u00a0Learning-Enabled Systems"],"prefix":"10.1007","author":[{"given":"Hoang-Dung","family":"Tran","sequence":"first","affiliation":[]},{"given":"Sung Woo","family":"Choi","sequence":"additional","affiliation":[]},{"given":"Yuntao","family":"Li","sequence":"additional","affiliation":[]},{"given":"Qing","family":"Liu","sequence":"additional","affiliation":[]},{"given":"Hideki","family":"Okamoto","sequence":"additional","affiliation":[]},{"given":"Bardh","family":"Hoxha","sequence":"additional","affiliation":[]},{"given":"Georgios","family":"Fainekos","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,7,22]]},"reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"Affonso, C., Rossi, A.L.D., Vieira, F.H.A., de Leon Ferreira, A.C.P., et al.: Deep learning for biological image classification. Expert Syst. Appl. 85, 114\u2013122 (2017)","DOI":"10.1016\/j.eswa.2017.05.039"},{"key":"17_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/978-3-030-72013-1_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Amir","year":"2021","unstructured":"Amir, G., Wu, H., Barrett, C., Katz, G.: An SMT-based approach for verifying binarized neural networks. In: TACAS 2021. LNCS, vol. 12652, pp. 203\u2013222. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_11"},{"key":"17_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-030-76384-8_2","volume-title":"NASA Formal Methods","author":"S Bak","year":"2021","unstructured":"Bak, S.: nnenum: verification of ReLU neural networks with optimized abstraction refinement. In: Dutle, A., Moscato, M.M., Titolo, L., Mu\u00f1oz, C.A., Perez, I. (eds.) NFM 2021. LNCS, vol. 12673, pp. 19\u201336. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-76384-8_2"},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"Bak, S., Duggirala, P.S.: HyLAA: a tool for computing simulation-equivalent reachability for linear systems. In: Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control, pp. 173\u2013178. ACM (2017)","DOI":"10.1145\/3049797.3049808"},{"key":"17_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/978-3-319-63387-9_20","volume-title":"Computer Aided Verification","author":"S Bak","year":"2017","unstructured":"Bak, S., Duggirala, P.S.: Simulation-equivalent reachability of large linear systems with inputs. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 401\u2013420. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_20"},{"key":"17_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/978-3-030-53288-8_4","volume-title":"Computer Aided Verification","author":"S Bak","year":"2020","unstructured":"Bak, S., Tran, H.-D., Hobbs, K., Johnson, T.T.: Improved geometric path enumeration for verifying ReLU neural networks. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 66\u201396. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_4"},{"key":"17_CR7","doi-asserted-by":"crossref","unstructured":"Bak, S., Tran, H.D., Johnson, T.T.: Numerical verification of affine systems with up to a billion dimensions. In: Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, pp. 23\u201332. ACM (2019)","DOI":"10.1145\/3302504.3311792"},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"Baluta, T., Shen, S., Shinde, S., Meel, K.S., Saxena, P.: Quantitative verification of neural networks and its security applications. In: Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, pp. 1249\u20131264 (2019)","DOI":"10.1145\/3319535.3354245"},{"key":"17_CR9","doi-asserted-by":"crossref","unstructured":"Brix, C., Bak, S., Liu, C., Johnson, T.T.: The fourth international verification of neural networks competition (VNN-comp 2023): summary and results. arXiv preprint arXiv:2312.16760 (2023)","DOI":"10.1007\/s10009-023-00703-4"},{"key":"17_CR10","unstructured":"Brix, C., Bak, S., Liu, C., Johnson, T.T.: The fourth international verification of neural networks competition (VNN-comp 2023): summary and results. arXiv:abs\/2312.16760 (2023). https:\/\/api.semanticscholar.org\/CorpusID:266572985"},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"Brown, R., Nguyen, L.V., Xiang, W., Wolf, M., Tran, H.D.: Perception-based quantitative runtime verification for learning-enabled cyber-physical systems. In: 2025 the 16th ACM\/IEEE International Conference on Cyber-Physical Systems (ICCPS), pp.1\u201311. ACM\/IEEE (2025)","DOI":"10.1145\/3716550.3722031"},{"key":"17_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3627991","volume":"24","author":"SW Choi","year":"2023","unstructured":"Choi, S.W., Ivashchenko, M., Nguyen, L.V., Tran, H.D.: Reachability analysis of sigmoidal neural networks. ACM Trans. Embed. Comput. Syst. 24, 1\u201325 (2023)","journal-title":"ACM Trans. Embed. Comput. Syst."},{"key":"17_CR13","doi-asserted-by":"publisher","DOI":"10.1016\/j.nahs.2025.101581","volume":"56","author":"SW Choi","year":"2025","unstructured":"Choi, S.W., et al.: Reachability analysis of recurrent neural networks. Hybrid Syst. Nonlinear Anal. 56, 101581 (2025)","journal-title":"Hybrid Syst. Nonlinear Anal."},{"key":"17_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/978-3-319-41528-4_26","volume-title":"Computer Aided Verification","author":"PS Duggirala","year":"2016","unstructured":"Duggirala, P.S., Viswanathan, M.: Parsimonious, simulation based verification of linear systems. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 477\u2013494. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_26"},{"key":"17_CR15","unstructured":"Duong, H., Li, L., Nguyen, T., Dwyer, M.: A DPLL (T) framework for verifying deep neural networks. arXiv preprint arXiv:2307.10266 (2023)"},{"key":"17_CR16","doi-asserted-by":"crossref","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, pp. 157\u2013168 (2019)","DOI":"10.1145\/3302504.3311807"},{"key":"17_CR17","doi-asserted-by":"publisher","first-page":"163938","DOI":"10.1109\/ACCESS.2021.3133370","volume":"9","author":"M Everett","year":"2021","unstructured":"Everett, M., Habibi, G., Sun, C., How, J.P.: Reachability analysis of neural feedback loops. IEEE Access 9, 163938\u2013163953 (2021)","journal-title":"IEEE Access"},{"key":"17_CR18","doi-asserted-by":"crossref","unstructured":"Fazlyab, M., Morari, M., Pappas, G.J.: Probabilistic verification and reachability analysis of neural networks via semidefinite programming. In: 2019 IEEE 58th Conference on Decision and Control (CDC), pp. 2726\u20132731. IEEE (2019)","DOI":"10.1109\/CDC40024.2019.9029310"},{"key":"17_CR19","first-page":"1","volume":"16","author":"M Fazlyab","year":"2020","unstructured":"Fazlyab, M., Morari, M., Pappas, G.J.: Safety verification and robustness analysis of neural networks via quadratic constraints and semidefinite programming. IEEE Trans. Autom. Control 16, 1\u20135 (2020)","journal-title":"IEEE Trans. Autom. Control"},{"key":"17_CR20","doi-asserted-by":"crossref","unstructured":"Ferlez, J., Khedr, H., Shoukry, Y.: Fast BATLLNN: fast box analysis of two-level lattice neural networks. In: Proceedings of the 25th ACM International Conference on Hybrid Systems: Computation and Control, pp. 1\u201311 (2022)","DOI":"10.1145\/3501710.3519533"},{"key":"17_CR21","doi-asserted-by":"publisher","unstructured":"Fischer, M., Sprecher, C., Dimitrov, D.I., Singh, G., Vechev, M.: Shared certificates for neural network verification. In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification. CAV 2022. LNCS, vol. 13371, pp. 127\u2013148. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_7","DOI":"10.1007\/978-3-031-13185-1_7"},{"key":"17_CR22","unstructured":"Girard-Satabin, J., Alberti, M., Bobot, F., Chihani, Z., Lemesle, A.: Caisar: a platform for characterizing artificial intelligence safety and robustness. arXiv preprint arXiv:2206.03044 (2022)"},{"key":"17_CR23","doi-asserted-by":"publisher","unstructured":"Goubault, E., Putot, S.: A zonotopic dempster-shafer approach to the quantitative verification of neural networks. In: Platzer, A., Rozier, K.Y., Pradella, M., Rossi, M. (eds.) Formal Methods. FM 2024. LNCS, vol. 14933, pp. 324\u2013342. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-71162-6_17","DOI":"10.1007\/978-3-031-71162-6_17"},{"issue":"11","key":"17_CR24","doi-asserted-by":"publisher","first-page":"4310","DOI":"10.1109\/TCAD.2024.3448306","volume":"43","author":"P Habeeb","year":"2024","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. 43(11), 4310\u20134321 (2024)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"17_CR25","doi-asserted-by":"crossref","unstructured":"Hashemi, N., Hoxha, B., Yamaguchi, T., Prokhorov, D., Fainekos, G., Deshmukh, J.: A neurosymbolic approach to the verification of temporal logic properties of learning-enabled control systems. In: Proceedings of the ACM\/IEEE 14th International Conference on Cyber-Physical Systems (with CPS-IoT Week 2023), pp. 98\u2013109 (2023)","DOI":"10.1145\/3576841.3585928"},{"issue":"11","key":"17_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)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"17_CR27","doi-asserted-by":"crossref","unstructured":"Hu, H., Fazlyab, M., Morari, M., Pappas, G.J.: Reach-SDP: reachability analysis of closed-loop systems with neural network controllers via semidefinite programming. In: 2020 59th IEEE Conference on Decision and Control (CDC), pp. 5929\u20135934. IEEE (2020)","DOI":"10.1109\/CDC42340.2020.9304296"},{"key":"17_CR28","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: Bouajjani, A., Hol\u00edk, L., Wu, Z. (eds.) Automated Technology for Verification and Analysis. ATVA 2022. LNCS, vol. 13505, pp. 414\u2013430. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-19992-9_27","DOI":"10.1007\/978-3-031-19992-9_27"},{"key":"17_CR29","doi-asserted-by":"crossref","unstructured":"Huang, C., Fan, J., Li, W., Chen, X., Zhu, Q.: Reachnn: Reachability analysis of neural-network controlled systems. arXiv preprint arXiv:1906.10654 (2019)","DOI":"10.1145\/3358228"},{"key":"17_CR30","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":"17_CR31","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. (eds.) CAV 2021. LNCS, vol. 12759, pp. 249\u2013262. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_11"},{"key":"17_CR32","doi-asserted-by":"crossref","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 (2020)","DOI":"10.1145\/3365365.3382216"},{"key":"17_CR33","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":"17_CR34","doi-asserted-by":"crossref","unstructured":"Ivashchenko, M., Choi, S.W., Nguyen, L.V., Tran, H.D.: Verifying binary neural networks on continuous input space using star reachability. In: 2023 IEEE\/ACM 11th International Conference on Formal Methods in Software Engineering (FormaliSE), pp. 7\u201317. IEEE (2023)","DOI":"10.1109\/FormaliSE58978.2023.00009"},{"key":"17_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/978-3-030-88806-0_10","volume-title":"Static Analysis","author":"K Jia","year":"2021","unstructured":"Jia, K., Rinard, M.: Verifying low-dimensional input neural networks via input quantization. In: Dr\u0103goi, C., Mukherjee, S., Namjoshi, K. (eds.) SAS 2021. LNCS, vol. 12913, pp. 206\u2013214. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-88806-0_10"},{"key":"17_CR36","doi-asserted-by":"crossref","unstructured":"Johnson, T.T., Met al.: Arch-comp20 category report: artificial intelligence and neural network control systems (AINNCS) for continuous and hybrid systems plants. EPiC Ser. Comput. 74, 107\u2013173 (2020)","DOI":"10.29007\/9xgv"},{"key":"17_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-319-63387-9_5","volume-title":"Computer Aided Verification","author":"G Katz","year":"2017","unstructured":"Katz, G., Barrett, C., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: an efficient SMT solver for verifying deep neural networks. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 97\u2013117. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_5"},{"key":"17_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/978-3-030-25540-4_26","volume-title":"Computer Aided Verification","author":"G Katz","year":"2019","unstructured":"Katz, G., et al.: The Marabou framework for verification and analysis of deep neural networks. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 443\u2013452. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_26"},{"key":"17_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-030-81685-8_13","volume-title":"Computer Aided Verification","author":"H Khedr","year":"2021","unstructured":"Khedr, H., Ferlez, J., Shoukry, Y.: PEREGRiNN: penalized-relaxation greedy neural network verifier. In: Silva, A., Leino, K. (eds.) CAV 2021. LNCS, vol. 12759, pp. 287\u2013300. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_13"},{"key":"17_CR40","doi-asserted-by":"publisher","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. NFM 2023. LNCS, vol. 13903, pp. 16\u201336. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-33170-1_2","DOI":"10.1007\/978-3-031-33170-1_2"},{"key":"17_CR41","unstructured":"Krizhevsky, A., Sutskever, I., Hinton, G.E.: Imagenet classification with deep convolutional neural networks. In: Advances in Neural Information Processing Systems, pp. 1097\u20131105 (2012)"},{"issue":"3\u20134","key":"17_CR42","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1561\/2400000035","volume":"4","author":"C Liu","year":"2021","unstructured":"Liu, C., Arnon, T., Lazarus, C., Strong, C., Barrett, C., Kochenderfer, M.J.: Algorithms for verifying deep neural networks. Found. Trends Optim. 4(3\u20134), 244\u2013404 (2021). https:\/\/doi.org\/10.1561\/2400000035","journal-title":"Found. Trends Optim."},{"key":"17_CR43","unstructured":"Lomuscio, A., Maganti, L.: An approach to reachability analysis for feed-forward ReLu neural networks. arXiv preprint arXiv:1706.07351 (2017)"},{"key":"17_CR44","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. CAV 2023. LNCS, vol. 13965, 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":"17_CR45","doi-asserted-by":"crossref","unstructured":"Mangal, R., Nori, A.V., Orso, A.: Robustness of neural networks: a probabilistic and practical approach. In: 2019 IEEE\/ACM 41st International Conference on Software Engineering: New Ideas and Emerging Results (ICSE-NIER), pp. 93\u201396. IEEE (2019)","DOI":"10.1109\/ICSE-NIER.2019.00032"},{"key":"17_CR46","doi-asserted-by":"publisher","unstructured":"Matthew\u00a0Sotoudeh, Z.T., Thakur, A.V.: SyReNN: a tool for analyzing deep neural networks. Int. J. Softw. Tools Technol .Transfer. 25, 145\u2013165 (2023). https:\/\/doi.org\/10.1007\/s10009-023-00695-1","DOI":"10.1007\/s10009-023-00695-1"},{"key":"17_CR47","doi-asserted-by":"publisher","unstructured":"Mitra, S., et al.: Formal verification techniques for vision-based autonomous systems\u2013a survey. In: Jansen, N., et al. (eds.) Principles of Verification: Cycling the Probabilistic Landscape: Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday, Part III, pp. 89\u2013108. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-75778-5_5","DOI":"10.1007\/978-3-031-75778-5_5"},{"issue":"7","key":"17_CR48","doi-asserted-by":"publisher","first-page":"4316","DOI":"10.1109\/TITS.2020.3032227","volume":"22","author":"K Muhammad","year":"2020","unstructured":"Muhammad, K., Ullah, A., Lloret, J., Del Ser, J., de Albuquerque, V.: Deep learning for safe autonomous driving: current challenges and future directions. IEEE Trans. Intell. Transp. Syst. 22(7), 4316\u20134336 (2020)","journal-title":"IEEE Trans. Intell. Transp. Syst."},{"key":"17_CR49","unstructured":"(ONNX), O.N.N.E. https:\/\/github.com\/onnx\/"},{"key":"17_CR50","doi-asserted-by":"crossref","unstructured":"Otter, D.W., Medina, J.R., Kalita, J.K.: A survey of the usages of deep learning for natural language processing. IEEE Trans. Neural Netw. Learn. Syst. 32(2), 604\u2013624 (2020)","DOI":"10.1109\/TNNLS.2020.2979670"},{"key":"17_CR51","doi-asserted-by":"crossref","unstructured":"P\u0103s\u0103reanu, C., Converse, H., Filieri, A., Gopinath, D.: On the probabilistic analysis of neural networks. In: Proceedings of the IEEE\/ACM 15th International Symposium on Software Engineering for Adaptive and Self-Managing Systems, pp.\u00a05\u20138 (2020)","DOI":"10.1145\/3387939.3391594"},{"key":"17_CR52","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. Lecture Notes in Computer Science, 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":"17_CR53","doi-asserted-by":"crossref","unstructured":"Pautov, M., Tursynbek, N., Munkhoeva, M., Muravev, N., Petiushko, A., Oseledets, I.: Cc-cert: a probabilistic approach to certify general robustness of neural networks. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol.\u00a036, pp. 7975\u20137983 (2022)","DOI":"10.1609\/aaai.v36i7.20768"},{"key":"17_CR54","unstructured":"Prabhakar, P., Rahimi\u00a0Afzal, Z.: Abstraction based output range analysis for neural networks. Adv. Neural Inf. Process. Syst. 32, 1\u201311 (2019)"},{"key":"17_CR55","doi-asserted-by":"crossref","unstructured":"Pramanik, A., Choi, S.W., Li, Y., Nguyen, L.V., Kim, K., Tran, H.D.: Perception-based runtime monitoring and verification for human-robot construction systems. In: 2024 22nd ACM-IEEE International Symposium on Formal Methods and Models for System Design (MEMOCODE), pp. 124\u2013134. IEEE (2024)","DOI":"10.1109\/MEMOCODE63347.2024.00021"},{"key":"17_CR56","doi-asserted-by":"publisher","unstructured":"Santa\u00a0Cruz, 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":"17_CR57","doi-asserted-by":"crossref","unstructured":"Schilling, C., Forets, M., Guadalupe, S.: Verification of neural-network control systems by integrating Taylor models and zonotopes. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol.\u00a036, pp. 8169\u20138177 (2022)","DOI":"10.1609\/aaai.v36i7.20790"},{"key":"17_CR58","doi-asserted-by":"crossref","unstructured":"Shih, A., Darwiche, A., Choi, A.: Verifying binarized neural networks by Angluin-style learning. In: SAT, pp. 354\u2013370 (2019). https:\/\/doi.org\/10.1007\/978-3-030-24258-9_25","DOI":"10.1007\/978-3-030-24258-9_25"},{"issue":"117","key":"17_CR59","first-page":"1","volume":"23","author":"C Sidrane","year":"2022","unstructured":"Sidrane, C., Maleki, A., Irfan, A., Kochenderfer, M.J.: Overt: an algorithm for safety verification of neural network control policies for nonlinear systems. J. Mach. Learn. Res. 23(117), 1\u201345 (2022)","journal-title":"J. Mach. Learn. Res."},{"key":"17_CR60","unstructured":"Simonyan, K., Zisserman, A.: Very deep convolutional networks for large-scale image recognition. arXiv preprint arXiv:1409.1556 (2014)"},{"key":"17_CR61","doi-asserted-by":"crossref","unstructured":"Singh, G., Gehr, T., P\u00fcschel, M., Vechev, M.: An abstract domain for certifying neural networks. Proc. ACM Program. Lang. 3(POPL), 41 (2019)","DOI":"10.1145\/3290354"},{"key":"17_CR62","doi-asserted-by":"publisher","unstructured":"Singh, G., Gehr, T., P\u00fcschel, M., Vechev, M.: An abstract domain for certifying neural networks. Proc. ACM Program. Lang. 3(POPL), 1\u201330 (2019). https:\/\/doi.org\/10.1145\/3290354","DOI":"10.1145\/3290354"},{"key":"17_CR63","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1016\/j.cogr.2023.04.001","volume":"3","author":"M Soori","year":"2023","unstructured":"Soori, M., Arezoo, B., Dastres, R.: Artificial intelligence, machine learning and deep learning in advanced robotics, a review. Cogn. Robot. 3, 54\u201370 (2023)","journal-title":"Cogn. Robot."},{"key":"17_CR64","doi-asserted-by":"crossref","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, pp. 147\u2013156 (2019)","DOI":"10.1145\/3302504.3311802"},{"key":"17_CR65","unstructured":"Szegedy, C., et al.: Intriguing properties of neural networks. arXiv preprint arXiv:1312.6199 (2013)"},{"key":"17_CR66","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/978-3-030-53288-8_2","volume-title":"Computer Aided Verification","author":"H-D Tran","year":"2020","unstructured":"Tran, H.-D., Bak, S., Xiang, W., Johnson, T.T.: Verification of deep convolutional neural networks using ImageStars. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 18\u201342. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_2"},{"issue":"5s","key":"17_CR67","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3358230","volume":"18","author":"HD Tran","year":"2019","unstructured":"Tran, H.D., Cai, F., Diego, M.L., Musau, P., Johnson, T.T., Koutsoukos, X.: Safety verification of cyber-physical systems with reinforcement learning control. ACM Trans. Embed. Comput. Syst. (TECS) 18(5s), 1\u201322 (2019)","journal-title":"ACM Trans. Embed. Comput. Syst. (TECS)"},{"key":"17_CR68","doi-asserted-by":"crossref","unstructured":"Tran, H.D., Cei, F., Lopez, D.M., Johnson, T.T., Koutsoukos, X.: Safety verification of cyber-physical systems with reinforcement learning control. In: ACM SIGBED International Conference on Embedded Software (EMSOFT 2019). ACM, October 2019","DOI":"10.1145\/3358230"},{"key":"17_CR69","doi-asserted-by":"crossref","unstructured":"Tran, H.D., Choi, S.W., Yang, X., Yamaguchi, T., Hoxha, B., Prokhorov, D.: Verification of recurrent neural networks with star reachability. In: Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control, pp. 1\u201313 (2023)","DOI":"10.1145\/3575870.3587128"},{"key":"17_CR70","doi-asserted-by":"crossref","unstructured":"Tran, H.D., Choi, S., Li, Y., Okamoto, H., Hoxha, B., Fainekos, G.: Probstar temporal logic for verifying complex behaviors of learning-enabled systems. In: Proceedings of the 28th ACM International Conference on Hybrid Systems: Computation and Control (2025)","DOI":"10.1145\/3716863.3718035"},{"key":"17_CR71","doi-asserted-by":"crossref","unstructured":"Tran, H.D., Choi, S., Okamoto, H., Hoxha, B., Fainekos, G., Prokhorov, D.: Quantitative verification for neural networks using probstars. In: Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control, pp. 1\u201312 (2023)","DOI":"10.1145\/3575870.3587112"},{"key":"17_CR72","doi-asserted-by":"crossref","unstructured":"Tran, H.D., Choi, S., Yamaguchi, T., Hoxha, B., Prokhorov, D.: Verification of recurrent neural networks using star reachability. In: The 26th ACM International Conference on Hybrid Systems: Computation and Control (HSCC), May 2023","DOI":"10.1145\/3575870.3587128"},{"key":"17_CR73","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"670","DOI":"10.1007\/978-3-030-30942-8_39","volume-title":"Formal Methods \u2013 The Next 30 Years","author":"H-D Tran","year":"2019","unstructured":"Tran, H.-D., et al.: Star-based reachability analysis of deep neural networks. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 670\u2013686. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30942-8_39"},{"key":"17_CR74","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-030-81685-8_12","volume-title":"Computer Aided Verification","author":"H-D Tran","year":"2021","unstructured":"Tran, H.-D., et al.: Robustness verification of semantic segmentation neural networks using relaxed reachability. In: Silva, A., Leino, K. (eds.) CAV 2021. LNCS, vol. 12759, pp. 263\u2013286. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_12"},{"key":"17_CR75","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1109\/MDAT.2020.3015712","volume":"39","author":"HD Tran","year":"2020","unstructured":"Tran, H.D., Xiang, W., Johnson, T.T.: Verification approaches for learning-enabled autonomous cyber-physical systems. IEEE Design Test 39, 24\u201334 (2020)","journal-title":"IEEE Design Test"},{"key":"17_CR76","doi-asserted-by":"crossref","unstructured":"Tran, H.D., et al.: NNV: The neural network verification tool for deep neural networks and learning-enabled cyber-physical systems. In: 32nd International Conference on Computer-Aided Verification (CAV), July 2020","DOI":"10.1007\/978-3-030-53288-8_1"},{"key":"17_CR77","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-53288-8_1","volume-title":"Computer Aided Verification","author":"H-D 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.) CAV 2020. LNCS, vol. 12224, pp. 3\u201317. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_1"},{"key":"17_CR78","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1186\/s13073-021-00968-x","volume":"13","author":"KA Tran","year":"2021","unstructured":"Tran, K.A., Kondrashova, O., Bradley, A., Williams, E.D., Pearson, J.V., Waddell, N.: Deep learning in cancer diagnosis, prognosis and treatment selection. Genome Med. 13, 1\u201317 (2021)","journal-title":"Genome Med."},{"key":"17_CR79","doi-asserted-by":"crossref","unstructured":"Ugare, S., Banerjee, D., Misailovic, S., Singh, G.: Incremental verification of neural networks. Proc. ACM Program. Lang. 7(PLDI), 1920\u20131945 (2023)","DOI":"10.1145\/3591299"},{"key":"17_CR80","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-81685-8_1","volume-title":"Computer Aided Verification","author":"M Usman","year":"2021","unstructured":"Usman, M., Gopinath, D., Sun, Y., Noller, Y., P\u0103s\u0103reanu, C.S.: NNrepair: constraint-based repair of\u00a0neural network classifiers. In: Silva, A., Leino, K. (eds.) CAV 2021. LNCS, vol. 12759, pp. 3\u201325. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_1"},{"key":"17_CR81","unstructured":"Wang, S., Pei, K., Whitehouse, J., Yang, J., Jana, S.: Formal security analysis of neural networks using symbolic intervals. arXiv preprint arXiv:1804.10829 (2018)"},{"key":"17_CR82","unstructured":"Wang, S., et al.: Beta-crown: efficient bound propagation with per-neuron split constraints for neural network robustness verification. In: Proceedings of the 35th International Conference on Neural Information Processing Systems. NIPS 2021, Curran Associates Inc., Red Hook, NY, USA (2024)"},{"key":"17_CR83","unstructured":"Webb, S., Rainforth, T., Teh, Y.W., Kumar, M.P.: A statistical approach to assessing neural network robustness. arXiv preprint arXiv:1811.07209 (2018)"},{"key":"17_CR84","unstructured":"Weng, L., et al.: Proven: Verifying robustness of neural networks with a probabilistic approach. In: International Conference on Machine Learning, pp. 6727\u20136736. PMLR (2019)"},{"key":"17_CR85","doi-asserted-by":"publisher","unstructured":"Wu, H., et\u00a0al.: Marabou 2.0: a versatile formal analyzer of neural networks. In: Gurfinkel, A., Ganesh, V. (eds.) Computer Aided Verification. CAV 2024. LNCS, vol. 14682, pp. 249\u2013264. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-65630-9_13","DOI":"10.1007\/978-3-031-65630-9_13"},{"key":"17_CR86","first-page":"1129","volume":"33","author":"K Xu","year":"2020","unstructured":"Xu, K., et al.: Automatic perturbation analysis for scalable certified robustness and beyond. Adv. Neural. Inf. Process. Syst. 33, 1129\u20131141 (2020)","journal-title":"Adv. Neural. Inf. Process. Syst."},{"key":"17_CR87","unstructured":"Xu, K., et al.: Fast and complete: enabling complete neural network verification with rapid and massively parallel incomplete verifiers (2021). https:\/\/arxiv.org\/abs\/2011.13824"},{"key":"17_CR88","doi-asserted-by":"publisher","unstructured":"Yang, X., Yamaguchi, T., Tran, H.D., Hoxha, B., Johnson, T.T., Prokhorov, D.: Neural network repair with reachability analysis. In: Bogomolov, S., Parker, D. (eds.) Formal Modeling and Analysis of Timed Systems. FORMATS 2022. LNCS, vol. 13465, pp. 221\u2013236. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-15839-1_13","DOI":"10.1007\/978-3-031-15839-1_13"},{"key":"17_CR89","unstructured":"Yang, X., Yamaguchi, T., Tran, H.D., Hoxha, B., Johnson, T.T., Prokhorov, D.: Reachability analysis of convolutional neural networks. arXiv preprint arXiv:2106.12074 (2021)"},{"issue":"9","key":"17_CR90","doi-asserted-by":"publisher","first-page":"5408","DOI":"10.1109\/TGRS.2018.2815613","volume":"56","author":"X Yang","year":"2018","unstructured":"Yang, X., Ye, Y., Li, X., Lau, R.Y., Zhang, X., Huang, X.: Hyperspectral image classification with deep learning models. IEEE Trans. Geosci. Remote Sens. 56(9), 5408\u20135423 (2018)","journal-title":"IEEE Trans. Geosci. Remote Sens."},{"key":"17_CR91","doi-asserted-by":"crossref","unstructured":"Zhang, C., Ruan, W., Xu, P.: Reachability analysis of neural network control systems. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol.\u00a037, pp. 15287\u201315295 (2023)","DOI":"10.1609\/aaai.v37i12.26783"},{"key":"17_CR92","unstructured":"Zhang, H., Weng, T.W., Chen, P.Y., Hsieh, C.J., Daniel, L.: Efficient neural network robustness certification with general activation functions. In: Advances in Neural Information Processing Systems, pp. 4944\u20134953 (2018)"},{"key":"17_CR93","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-030-81685-8_8","volume-title":"Computer Aided Verification","author":"Y Zhang","year":"2021","unstructured":"Zhang, Y., Zhao, Z., Chen, G., Song, F., Chen, T.: BDD4BNN: a BDD-based quantitative analysis framework for binarized neural networks. In: Silva, A., Leino, K. (eds.) CAV 2021. LNCS, vol. 12759, pp. 175\u2013200. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_8"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-98679-6_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,7]],"date-time":"2025-09-07T16:18:55Z","timestamp":1757261935000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98679-6_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986789","9783031986796"],"references-count":93,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98679-6_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"22 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided 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":"25 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"37","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conferences.i-cav.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}