{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,5]],"date-time":"2026-05-05T04:58:36Z","timestamp":1777957116623,"version":"3.51.4"},"publisher-location":"Cham","reference-count":53,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031986789","type":"print"},{"value":"9783031986796","type":"electronic"}],"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>Deep Neural Networks (DNN) are crucial in approximating nonlinear functions across diverse applications, ranging from image classification to control. Verifying specific input-output properties can be a highly challenging task due to the lack of a single, self-contained framework that allows a complete range of various model architecture and input-output properties. To this end, we present  (<jats:ext-link xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" xlink:href=\"https:\/\/github.com\/intelligent-control-lab\/ModelVerification.jl\" ext-link-type=\"uri\">https:\/\/github.com\/intelligent-control-lab\/ModelVerification.jl<\/jats:ext-link>), the first comprehensive, cutting-edge toolbox that contains a suite of state-of-the-art methods for verifying different types of DNNs and input-output specifications. This versatile toolbox is designed to empower developers and machine learning practitioners with robust tools for verifying and ensuring the trustworthiness of their DNN models.<\/jats:p>","DOI":"10.1007\/978-3-031-98679-6_18","type":"book-chapter","created":{"date-parts":[[2025,7,21]],"date-time":"2025-07-21T09:20:36Z","timestamp":1753089636000},"page":"395-408","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["ModelVerification.jl: A\u00a0Comprehensive Toolbox for\u00a0Formally Verifying Deep Neural Networks"],"prefix":"10.1007","author":[{"given":"Tianhao","family":"Wei","sequence":"first","affiliation":[]},{"given":"Hanjiang","family":"Hu","sequence":"additional","affiliation":[]},{"given":"Luca","family":"Marzari","sequence":"additional","affiliation":[]},{"given":"Kai S.","family":"Yun","sequence":"additional","affiliation":[]},{"given":"Peizhi","family":"Niu","sequence":"additional","affiliation":[]},{"given":"Xusheng","family":"Luo","sequence":"additional","affiliation":[]},{"given":"Changliu","family":"Liu","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,7,22]]},"reference":[{"key":"18_CR1","doi-asserted-by":"publisher","unstructured":"Amir, G., Corsi, D., Yerushalmi, R., Marzari, L., Harel, D., Farinelli, A., Katz, G.: Verifying learning-based robotic navigation systems. In: 29th International Conference, TACAS 2023, pp. 607\u2013627. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_31","DOI":"10.1007\/978-3-031-30823-9_31"},{"key":"18_CR2","unstructured":"Bastani, O., Ioannou, Y., Lampropoulos, L., Vytiniotis, D., Nori, A., Criminisi, A.: Measuring neural net robustness with constraints. Adv. Neural Inf. Process. Syst. 29 (2016)"},{"issue":"1","key":"18_CR3","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1137\/141000671","volume":"59","author":"J Bezanson","year":"2017","unstructured":"Bezanson, J., Edelman, A., Karpinski, S., Shah, V.B.: Julia: a fresh approach to numerical computing. SIAM Rev. 59(1), 65\u201398 (2017)","journal-title":"SIAM Rev."},{"key":"18_CR4","doi-asserted-by":"crossref","unstructured":"Botoeva, E., Kouvaros, P., Kronqvist, J., Lomuscio, A., Misener, R.: Efficient verification of relu-based neural networks via dependency analysis. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol.\u00a034, pp. 3291\u20133299 (2020)","DOI":"10.1609\/aaai.v34i04.5729"},{"key":"18_CR5","doi-asserted-by":"crossref","unstructured":"Brix, C., M\u00fcller, M.N., Bak, S., Johnson, T.T., Liu, C.: First three years of the international verification of neural networks competition (vnn-comp). Int. J. Softw. Tools Technol. Transf., 1\u201311 (2023)","DOI":"10.1007\/s10009-023-00703-4"},{"key":"18_CR6","doi-asserted-by":"crossref","unstructured":"Chen, C., Seff, A., Kornhauser, A., Xiao, J.: Deepdriving: learning affordance for direct perception in autonomous driving. In: Proceedings of the IEEE International Conference on Computer Vision, pp. 2722\u20132730 (2015)","DOI":"10.1109\/ICCV.2015.312"},{"key":"18_CR7","unstructured":"Cheng, H., Hu, H., Liu, C.: Robust tracking control with neural network dynamic models under input perturbations. arXiv preprint arXiv:2410.10387 (2024)"},{"key":"18_CR8","first-page":"5318","volume":"33","author":"S Dathathri","year":"2020","unstructured":"Dathathri, S., et al.: Enabling certification of verification-agnostic networks via memory-efficient semidefinite programming. Adv. Neural. Inf. Process. Syst. 33, 5318\u20135331 (2020)","journal-title":"Adv. Neural. Inf. Process. Syst."},{"key":"18_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-319-77935-5_9","volume-title":"NASA Formal Methods","author":"S Dutta","year":"2018","unstructured":"Dutta, S., Jha, S., Sankaranarayanan, S., Tiwari, A.: Output range analysis for deep feedforward neural networks. In: Dutle, A., Mu\u00f1oz, C., Narkawicz, A. (eds.) NFM 2018. LNCS, vol. 10811, pp. 121\u2013138. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-77935-5_9"},{"key":"18_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"537","DOI":"10.1007\/978-3-030-59152-6_30","volume-title":"Automated Technology for Verification and Analysis","author":"J Fan","year":"2020","unstructured":"Fan, J., Huang, C., Chen, X., Li, W., Zhu, Q.: ReachNN*: a tool for reachability analysis of neural-network controlled systems. In: Hung, D.V., Sokolsky, O. (eds.) ATVA 2020. LNCS, vol. 12302, pp. 537\u2013542. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-59152-6_30"},{"key":"18_CR11","unstructured":"Ferrari, C., Muller, M.N., Jovanovic, N., Vechev, M.: Complete verification via multi-neuron relaxation guided branch-and-bound. arXiv preprint arXiv:2205.00263 (2022)"},{"key":"18_CR12","unstructured":"Forets, M., Schilling, C.: Lazysets. jl: scalable symbolic-numeric set computations. arXiv preprint arXiv:2110.01711 (2021)"},{"key":"18_CR13","doi-asserted-by":"crossref","unstructured":"Gatys, L.A., Ecker, A.S., Bethge, M.: Image style transfer using convolutional neural networks. In: Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition, pp. 2414\u20132423 (2016)","DOI":"10.1109\/CVPR.2016.265"},{"key":"18_CR14","doi-asserted-by":"crossref","unstructured":"Gehr, T., Mirman, M., Drachsler-Cohen, D., Tsankov, P., Chaudhuri, S., Vechev, M.: Ai2: safety and robustness certification of neural networks with abstract interpretation. In: 2018 IEEE Symposium on Security and Privacy (SP), pp. 3\u201318. IEEE (2018)","DOI":"10.1109\/SP.2018.00058"},{"key":"18_CR15","doi-asserted-by":"publisher","unstructured":"Goubault, E., Putot, S.: Rino: robust inner and outer approximated reachability of neural networks controlled systems. In: International Conference on Computer Aided Verification, pp. 511\u2013523. Springer, Heidelberg (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_25","DOI":"10.1007\/978-3-031-13185-1_25"},{"key":"18_CR16","doi-asserted-by":"crossref","unstructured":"Han, Y., Yang, S., Wang, W., Liu, J.: From design draft to real attire: unaligned fashion image translation. In: Proceedings of the 28th ACM International Conference on Multimedia, pp. 1533\u20131541 (2020)","DOI":"10.1145\/3394171.3413953"},{"key":"18_CR17","doi-asserted-by":"crossref","unstructured":"He, K., Zhang, X., Ren, S., Sun, J.: Deep residual learning for image recognition. In: Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition, pp. 770\u2013778 (2016)","DOI":"10.1109\/CVPR.2016.90"},{"key":"18_CR18","doi-asserted-by":"publisher","DOI":"10.1016\/j.rcim.2022.102522","volume":"82","author":"S He","year":"2023","unstructured":"He, S., Zhao, W., Hu, C., Zhu, Y., Liu, C.: A hierarchical long short term safety framework for efficient robot manipulation under uncertainty. Rob. Comput.-Integrat. Manuf. 82, 102522 (2023)","journal-title":"Rob. Comput.-Integrat. Manuf."},{"key":"18_CR19","doi-asserted-by":"crossref","unstructured":"Henriksen, P., Lomuscio, A.: Efficient neural network verification via adaptive refinement and adversarial search. In: ECAI 2020, pp. 2513\u20132520. IOS Press (2020)","DOI":"10.3233\/FAIA200385"},{"key":"18_CR20","unstructured":"Hu, H., Yang, Y., Wei, T., Liu, C.: Verification of neural control barrier functions with symbolic derivative bounds propagation. In: 8th Annual Conference on Robot Learning (2024). https:\/\/openreview.net\/forum?id=jnubz7wB2w"},{"key":"18_CR21","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":"18_CR22","doi-asserted-by":"crossref","unstructured":"Katz, G., et\u00a0al.: The marabou framework for verification and analysis of deep neural networks. In: International Conference on Computer Aided Verification (2019)","DOI":"10.1007\/978-3-030-25540-4_26"},{"key":"18_CR23","unstructured":"Krizhevsky, A., Hinton, G., et\u00a0al.: Learning multiple layers of features from tiny images (2009)"},{"key":"18_CR24","unstructured":"Krizhevsky, A., Sutskever, I., Hinton, G.E.: Imagenet classification with deep convolutional neural networks. Adv. Neural Inf. Process. Syst. 25 (2012)"},{"key":"18_CR25","doi-asserted-by":"crossref","unstructured":"Li, G., Xie, Y., Wei, T., Wang, K., Lin, L.: Flow guided recurrent neural encoder for video salient object detection. In: Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition, pp. 3243\u20133252 (2018)","DOI":"10.1109\/CVPR.2018.00342"},{"key":"18_CR26","doi-asserted-by":"crossref","unstructured":"Liu, C., Arnon, T., Lazarus, C., Strong, C., Barrett, C., Kochenderfer, M.J., et\u00a0al.: Algorithms for verifying deep neural networks. Found. Trends\u00ae Optim. 4(3-4), 244\u2013404 (2021)","DOI":"10.1561\/2400000035"},{"key":"18_CR27","unstructured":"Liu, S., Liu, C., Dolan, J.: Safe control under input limits with neural control barrier functions. In: Conference on Robot Learning, pp. 1970\u20131980. PMLR (2023)"},{"key":"18_CR28","unstructured":"Lomuscio, A., Maganti, L.: An approach to reachability analysis for feed-forward relu neural networks. arXiv preprint arXiv:1706.07351 (2017)"},{"key":"18_CR29","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: International Conference on Computer Aided Verification, pp. 397\u2013412. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-37703-7_19","DOI":"10.1007\/978-3-031-37703-7_19"},{"key":"18_CR30","unstructured":"Luo, X., et al.: Certifying robustness of learning-based keypoint detection and pose estimation methods. arXiv preprint arXiv:2408.00117 (2024)"},{"key":"18_CR31","doi-asserted-by":"publisher","unstructured":"Manzanas\u00a0Lopez, D., Musau, P., Hamilton, N.P., Johnson, T.T.: Reachability analysis of a general class of neural ordinary differential equations. In: International Conference on Formal Modeling and Analysis of Timed Systems, pp. 258\u2013277. Springer, Heidelberg (2022). https:\/\/doi.org\/10.1007\/978-3-031-15839-1_15","DOI":"10.1007\/978-3-031-15839-1_15"},{"key":"18_CR32","doi-asserted-by":"crossref","unstructured":"Marzari, L., Corsi, D., Cicalese, F., Farinelli, A.: The #dnn-verification problem: counting unsafe inputs for deep neural networks. In: International Joint Conference on Artificial Intelligence (IJCAI), pp. 217\u2013224 (2023)","DOI":"10.24963\/ijcai.2023\/25"},{"key":"18_CR33","doi-asserted-by":"crossref","unstructured":"Marzari, L., Corsi, D., Marchesini, E., Alessandro, F., Cicalese, F.: Enumerating safe regions in deep neural networks with provable probabilistic guarantees. In: Proceedings of the AAAI Conference on Artificial Intelligence (2024)","DOI":"10.1609\/aaai.v38i19.30134"},{"key":"18_CR34","doi-asserted-by":"crossref","unstructured":"Marzari, L., Corsi, D., Marchesini, E., Farinelli, A.: Curriculum learning for safe mapless navigation. In: Proceedings of the 37th ACM\/SIGAPP Symposium on Applied Computing, pp. 766\u2013769 (2022)","DOI":"10.1145\/3477314.3507182"},{"key":"18_CR35","doi-asserted-by":"crossref","unstructured":"Marzari, L., Pore, A., Dall\u2019Alba, D., Aragon-Camarasa, G., Farinelli, A., Fiorini, P.: Towards hierarchical task decomposition using deep reinforcement learning for pick and place subtasks. In: 2021 20th International Conference on Advanced Robotics (ICAR), pp. 640\u2013645. IEEE (2021)","DOI":"10.1109\/ICAR53236.2021.9659344"},{"key":"18_CR36","unstructured":"M\u00fcller, M.N., Brix, C., Bak, S., Liu, C., Johnson, T.T.: The third international verification of neural networks competition (vnn-comp 2022): summary and results. arXiv preprint arXiv:2212.10376 (2022)"},{"key":"18_CR37","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":"18_CR38","unstructured":"Singh, G., Ganvir, R., P\u00fcschel, M., Vechev, M.: Beyond the single neuron convex barrier for neural network certification. Adv. Neural Inf. Process. Syst. 32 (2019)"},{"key":"18_CR39","unstructured":"Szegedy, C., et al.: Intriguing properties of neural networks. arXiv preprint arXiv:1312.6199 (2013)"},{"key":"18_CR40","doi-asserted-by":"crossref","unstructured":"Tai, L., Paolo, G., Liu, M.: Virtual-to-real drl: continuous control of mobile robots for mapless navigation. In: IROS (2017)","DOI":"10.1109\/IROS.2017.8202134"},{"key":"18_CR41","unstructured":"Tjeng, V., Xiao, K.Y., Tedrake, R.: Evaluating robustness of neural networks with mixed integer programming. In: International Conference on Learning Representations (2018)"},{"key":"18_CR42","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"},{"key":"18_CR43","unstructured":"Wang, S., et al.: Beta-CROWN: efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification. Adv. Neural Inf. Process. Syst. 34 (2021)"},{"key":"18_CR44","doi-asserted-by":"crossref","unstructured":"Wei, T., Liu, C.: Safe control algorithms using energy functions: a uni ed framework, benchmark, and new directions. In: 2019 IEEE 58th Conference on Decision and Control (CDC), pp. 238\u2013243. IEEE (2019)","DOI":"10.1109\/CDC40024.2019.9029720"},{"key":"18_CR45","unstructured":"Wei, T., Liu, C.: Safe control with neural network dynamic models. In: Learning for Dynamics and Control Conference, pp. 739\u2013750. PMLR (2022)"},{"key":"18_CR46","unstructured":"Wei, T., Ma, L., Chen, R., Zhao, W., Liu, C.: Meta-control: automatic model-based control synthesis for heterogeneous robot skills. In: 8th Annual Conference on Robot Learning (2024). https:\/\/openreview.net\/forum?id=cvVEkS5yij"},{"key":"18_CR47","unstructured":"Xiang, W., Johnson, T.T.: Reachability analysis and safety verification for neural network control systems. arXiv preprint arXiv:1805.09944 (2018)"},{"key":"18_CR48","unstructured":"Xiang, W., Tran, H.D., Johnson, T.T.: Reachable set computation and safety verification for neural networks with relu activations. arXiv preprint arXiv:1712.08163 (2017)"},{"key":"18_CR49","unstructured":"Xu, K., et al.: Fast and complete: enabling complete neural network verification with rapid and massively parallel incomplete verifiers. In: International Conference on Learning Representations (2021). https:\/\/openreview.net\/forum?id=nVZtXBI6LNn"},{"key":"18_CR50","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: International Conference on Formal Modeling and Analysis of Timed Systems, pp. 221\u2013236. Springer, Heidelberg (2022). https:\/\/doi.org\/10.1007\/978-3-031-15839-1_13","DOI":"10.1007\/978-3-031-15839-1_13"},{"key":"18_CR51","doi-asserted-by":"crossref","unstructured":"Yang, Y., Hu, H., Wei, T., Li, S.E., Liu, C.: Scalable synthesis of formally verified neural value function for hamilton-jacobi reachability analysis. arXiv preprint arXiv:2407.20532 (2024)","DOI":"10.1613\/jair.1.16946"},{"key":"18_CR52","unstructured":"Zhang, H., et al.: General cutting planes for bound-propagation-based neural network verification. Adv. Neural Inf. Process. Syst. (2022)"},{"key":"18_CR53","unstructured":"Zhang, H., Weng, T.W., Chen, P.Y., Hsieh, C.J., Daniel, L.: Efficient neural network robustness certification with general activation functions. Adv. Neural Inf. Process. Syst. 31, 4939\u20134948 (2018). https:\/\/arxiv.org\/pdf\/1811.00866.pdf"}],"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_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,7]],"date-time":"2025-09-07T16:19:27Z","timestamp":1757261967000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98679-6_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986789","9783031986796"],"references-count":53,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98679-6_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"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"}}]}}