{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T07:01:32Z","timestamp":1779087692627,"version":"3.51.4"},"publisher-location":"Cham","reference-count":90,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031377020","type":"print"},{"value":"9783031377037","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,7,18]],"date-time":"2023-07-18T00:00:00Z","timestamp":1689638400000},"content-version":"vor","delay-in-days":198,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This manuscript presents the updated version of the Neural Network Verification (NNV) tool. NNV is a formal verification software tool for deep learning models and cyber-physical systems with neural network components. NNV was first introduced as a verification framework for feedforward and convolutional neural networks, as well as for neural network control systems. Since then, numerous works have made significant improvements in the verification of new deep learning models, as well as tackling some of the scalability issues that may arise when verifying complex models. In this new version of NNV, we introduce verification support for multiple deep learning models, including neural ordinary differential equations, semantic segmentation networks and recurrent neural networks, as well as a collection of reachability methods that aim to reduce the computation cost of reachability analysis of complex neural networks. We have also added direct support for standard input verification formats in the community such as VNNLIB (verification properties), and ONNX (neural networks) formats. We present a collection of experiments in which NNV verifies safety and robustness properties of feedforward, convolutional, semantic segmentation and recurrent neural networks, as well as neural ordinary differential equations and neural network control systems. Furthermore, we demonstrate the capabilities of NNV against a commercially available product in a collection of benchmarks from control systems, semantic segmentation, image classification, and time-series data.<\/jats:p>","DOI":"10.1007\/978-3-031-37703-7_19","type":"book-chapter","created":{"date-parts":[[2023,7,17]],"date-time":"2023-07-17T17:02:15Z","timestamp":1689613335000},"page":"397-412","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":36,"title":["NNV 2.0: The Neural Network Verification Tool"],"prefix":"10.1007","author":[{"given":"Diego Manzanas","family":"Lopez","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sung Woo","family":"Choi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hoang-Dung","family":"Tran","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Taylor T.","family":"Johnson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,7,18]]},"reference":[{"key":"19_CR1","unstructured":"Akintunde, M.E., Botoeva, E., Kouvaros, P., Lomuscio, A.: Formal verification of neural agents in non-deterministic environments. In: Proceedings of the 19th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2020), IFAAMAS 2020, . ACM, Auckland (2020)"},{"key":"19_CR2","doi-asserted-by":"crossref","unstructured":"Akintunde, M.E., Kevorchian, A., Lomuscio, A., Pirovano, E.: Verification of rnn-based neural agent-environment systems. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol. 33, pp. 6006\u20136013 (2019)","DOI":"10.1609\/aaai.v33i01.33016006"},{"key":"19_CR3","unstructured":"Althoff, M.: An introduction to cora 2015. In: Proceedings of the Workshop on Applied Verification for Continuous and Hybrid Systems (2015)"},{"key":"19_CR4","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":"19_CR5","doi-asserted-by":"crossref","unstructured":"Bak, S., Bogomolov, S., Johnson, T.T.: Hyst: a source transformation and translation tool for hybrid automaton models. In: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, pp. 128\u2013133. ACM (2015)","DOI":"10.1145\/2728606.2728630"},{"key":"19_CR6","unstructured":"Bak, S., Liu, C., Johnson, T.T.: The second international verification of neural networks competition (VNN-COMP 2021): Summary and results. CoRR abs\/2109.00498 (2021)"},{"key":"19_CR7","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":"19_CR8","doi-asserted-by":"crossref","unstructured":"Bogomolov, S., Forets, M., Frehse, G., Potomkin, K., Schilling, C.: Juliareach: a toolbox for set-based reachability. In: Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, pp. 39\u201344 (2019)","DOI":"10.1145\/3302504.3311804"},{"key":"19_CR9","unstructured":"Bojarski, M., et al.: End to end learning for self-driving cars. arXiv preprint arXiv:1604.07316 (2016)"},{"key":"19_CR10","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":"19_CR11","unstructured":"Chen, R.T.Q., Rubanova, Y., Bettencourt, J., Duvenaud, D.: Neural ordinary differential equations. Adv. Neural Inf. Process. Syst. (2018)"},{"key":"19_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-642-39799-8_18","volume-title":"Computer Aided Verification","author":"X Chen","year":"2013","unstructured":"Chen, X., \u00c1brah\u00e1m, E., Sankaranarayanan, S.: Flow*: an analyzer for non-linear hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 258\u2013263. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_18"},{"key":"19_CR13","doi-asserted-by":"crossref","unstructured":"Cire\u015fan, D., Meier, U., Schmidhuber, J.: Multi-column deep neural networks for image classification. arXiv preprint arXiv:1202.2745 (2012)","DOI":"10.1109\/CVPR.2012.6248110"},{"key":"19_CR14","unstructured":"Cohen, J., Rosenfeld, E., Kolter, Z.: Certified adversarial robustness via randomized smoothing. In: Chaudhuri, K., Salakhutdinov, R. (eds.) Proceedings of the 36th International Conference on Machine Learning. Proceedings of Machine Learning Research, vol. 97, pp. 1310\u20131320. PMLR (2019)"},{"key":"19_CR15","doi-asserted-by":"crossref","unstructured":"Collobert, R., Weston, J.: A unified architecture for natural language processing: Deep neural networks with multitask learning. In: Proceedings of the 25th International Conference on Machine Learning, pp. 160\u2013167. ACM (2008)","DOI":"10.1145\/1390156.1390177"},{"key":"19_CR16","doi-asserted-by":"crossref","unstructured":"Dutta, S., Jha, S., Sankaranarayanan, S., Tiwari, A.: Output range analysis for deep feedforward neural networks, pp. 121\u2013138 (2018)","DOI":"10.1007\/978-3-319-77935-5_9"},{"key":"19_CR17","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":"19_CR18","unstructured":"(farhanhubble), F.A.: M2NIST, MNIST of semantic segmentation. https:\/\/www.kaggle.com\/datasets\/farhanhubble\/multimnistm2nist"},{"key":"19_CR19","doi-asserted-by":"crossref","unstructured":"Ferlez, J., Khedr, H., Shoukry, Y.: Fast BATLLNN: fast box analysis of two-level lattice neural networks. In: Bartocci, E., Putot, S. (eds.) HSCC \u201922: 25th ACM International Conference on Hybrid Systems: Computation and Control, Milan, Italy, 4\u20136 May 2022. pp. 23:1\u201323:11. ACM (2022)","DOI":"10.1145\/3501710.3519533"},{"key":"19_CR20","unstructured":"Ferrari, C., M\u00fcller, M.N., Jovanovic, N., Vechev, M.T.: Complete verification via multi-neuron relaxation guided branch-and-bound. In: The Tenth International Conference on Learning Representations, ICLR 2022, Virtual Event, 25\u201329 April 2022. OpenReview.net (2022)"},{"key":"19_CR21","unstructured":"Fischer, M., Baader, M., Vechev, M.: Scalable certified segmentation via randomized smoothing. In: Meila, M., Zhang, T. (eds.) Proceedings of the 38th International Conference on Machine Learning. Proceedings of Machine Learning Research, vol. 139, pp. 3340\u20133351. PMLR (2021)"},{"key":"19_CR22","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/978-3-031-13185-1_7","volume-title":"Computer Aided Verification","author":"M Fischer","year":"2022","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, pp. 127\u2013148. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_7"},{"key":"19_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/978-3-642-22110-1_30","volume-title":"Computer Aided Verification","author":"G Frehse","year":"2011","unstructured":"Frehse, G., et al.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379\u2013395. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_30"},{"key":"19_CR24","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":"19_CR25","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1613\/jair.4992","volume":"57","author":"Y Goldberg","year":"2016","unstructured":"Goldberg, Y.: A primer on neural network models for natural language processing. J. Artif. Intell. Res. 57, 345\u2013420 (2016)","journal-title":"J. Artif. Intell. Res."},{"key":"19_CR26","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1007\/978-3-031-13185-1_25","volume-title":"Computer Aided Verification","author":"E Goubault","year":"2022","unstructured":"Goubault, E., Putot, S.: Rino: Robust inner and outer approximated reachability of neural networks controlled systems. In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification, pp. 511\u2013523. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_25"},{"key":"19_CR27","doi-asserted-by":"crossref","unstructured":"Gruenbacher, S., Hasani, R.M., Lechner, M., Cyranka, J., Smolka, S.A., Grosu, R.: On the verification of neural odes with stochastic guarantees. In: AAAI (2021)","DOI":"10.1609\/aaai.v35i13.17372"},{"key":"19_CR28","unstructured":"Gruenbacher, S., et al.: Gotube: scalable stochastic verification of continuous-depth models (2021)"},{"key":"19_CR29","unstructured":"Guidotti, D., Demarchi, S., Tacchella, A., Pulina, L.: The Verification of Neural Networks Library (VNN-LIB) (2022). https:\/\/www.vnnlib.org"},{"key":"19_CR30","doi-asserted-by":"crossref","unstructured":"He, K., Zhang, X., Ren, S., Sun, J.: Deep residual learning for image recognition. In: 2016 IEEE Conference on Computer Vision and Pattern Recognition (CVPR), pp. 770\u2013778 (2016)","DOI":"10.1109\/CVPR.2016.90"},{"key":"19_CR31","unstructured":"Henriksen, P., Hammernik, K., Rueckert, D., Lomuscio, A.: Bias field robustness verification of large neural image classifiers. In: Proceedings of the 32nd British Machine Vision Conference (BMVC21). BMVA Press (2021)"},{"key":"19_CR32","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 (2021). https:\/\/doi.org\/10.48550\/ARXIV.2106.13867","DOI":"10.48550\/ARXIV.2106.13867"},{"key":"19_CR33","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":"19_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-030-81685-8_11","volume-title":"Computer Aided Verification","author":"R Ivanov","year":"2021","unstructured":"Ivanov, R., Carpenter, T., Weimer, J., Alur, R., Pappas, G., Lee, I.: Verisig 2.0: verification of neural network controllers using taylor model preconditioning. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 249\u2013262. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_11"},{"key":"19_CR35","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: Hybrid Systems: Computation and Control (HSCC) (2019)","DOI":"10.1145\/3302504.3311806"},{"key":"19_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/978-3-030-59152-6_3","volume-title":"Automated Technology for Verification and Analysis","author":"Y Jacoby","year":"2020","unstructured":"Jacoby, Y., Barrett, C., Katz, G.: Verifying recurrent neural networks using invariant inference. In: Hung, D.V., Sokolsky, O. (eds.) ATVA 2020. LNCS, vol. 12302, pp. 57\u201374. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-59152-6_3"},{"key":"19_CR37","doi-asserted-by":"crossref","unstructured":"Jain, L.C., Medsker, L.R.: Recurrent neural networks: design and applications (1999)","DOI":"10.1201\/9781420049176"},{"key":"19_CR38","doi-asserted-by":"publisher","unstructured":"Johnson, T.T., et al.: Arch-comp21 category report: artificial intelligence and neural network control systems (ainncs) for continuous and hybrid systems plants. In: Frehse, G., Althoff, M. (eds.) 8th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH21). EPiC Series in Computing, vol. 80, pp. 90\u2013119. EasyChair (2021). https:\/\/doi.org\/10.29007\/kfk9","DOI":"10.29007\/kfk9"},{"key":"19_CR39","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":"19_CR40","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":"19_CR41","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.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 287\u2013300. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_13"},{"key":"19_CR42","doi-asserted-by":"crossref","unstructured":"Kochdumper, N., Schilling, C., Althoff, M., Bak, S.: Open- and closed-loop neural network verification using polynomial zonotopes (2022)","DOI":"10.1007\/978-3-031-33170-1_2"},{"key":"19_CR43","unstructured":"Krizhevsky, A.: Learning multiple layers of features from tiny images, pp. 32\u201333 (2009)"},{"key":"19_CR44","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)"},{"key":"19_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"448","DOI":"10.1007\/978-3-540-24743-2_30","volume-title":"Hybrid Systems: Computation and Control","author":"M Kvasnica","year":"2004","unstructured":"Kvasnica, M., Grieder, P., Baoti\u0107, M., Morari, M.: Multi-parametric toolbox (MPT). In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 448\u2013462. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24743-2_30"},{"key":"19_CR46","unstructured":"LeCun, Y.: The mnist database of handwritten digits (1998). http:\/\/yann.lecun.com\/exdb\/mnist\/"},{"key":"19_CR47","unstructured":"Lenz, I.: Deep learning for robotics. Ph.D. thesis, Cornell University (2016)"},{"issue":"3\u20134","key":"19_CR48","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":"19_CR49","unstructured":"L\u00f6fberg, J.: Yalmip : A toolbox for modeling and optimization in MATLAB. In: Proceedings of the CACSD Conference, Taipei, Taiwan (2004). http:\/\/users.isy.liu.se\/johanl\/yalmip"},{"key":"19_CR50","unstructured":"Lopez, D.M., et al.: Arch-comp22 category report: artificial intelligence and neural network control systems (ainncs) for continuous and hybrid systems plants. In: Frehse, G., Althoff, M., Schoitsch, E., Guiochet, J. (eds.) Proceedings of 9th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH22). EPiC Series in Computing, vol. 90, pp. 142\u2013184. EasyChair (2022)"},{"key":"19_CR51","unstructured":"Lopez, D.M., Johnson, T.T., Bak, S., Tran, H.D., Hobbs, K.: Evaluation of neural network verification methods for air to air collision avoidance. AIAA J. Air Transp. (JAT) (2022)"},{"key":"19_CR52","doi-asserted-by":"crossref","unstructured":"Manzanas Lopez, D., Musau, P., Hamilton, N., Johnson, T.: Reachability analysis of a general class of neural ordinary differential equation. In: Proceedings of the 20th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2022), Co-Located with CONCUR, FMICS, and QEST as part of CONFEST 2022, Warsaw, Poland (2022)","DOI":"10.1007\/978-3-031-15839-1_15"},{"key":"19_CR53","unstructured":"MATLAB: Update 3, (R2022b). The MathWorks Inc., Natick, Massachusetts (2022)"},{"key":"19_CR54","doi-asserted-by":"crossref","unstructured":"Musau, P., Johnson, T.T.: Continuous-time recurrent neural networks (ctrnns) (benchmark proposal). In: 5th Applied Verification for Continuous and Hybrid Systems Workshop (ARCH), Oxford, UK (2018). https:\/\/doi.org\/10.29007\/6czp","DOI":"10.29007\/6czp"},{"key":"19_CR55","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 (2022)"},{"key":"19_CR56","unstructured":"Oki, E.: Glpk (gnu linear programming kit) (2012)"},{"key":"19_CR57","unstructured":"(ONNX), O.N.N.E.: https:\/\/github.com\/onnx\/"},{"key":"19_CR58","unstructured":"O\u2019Shea, K., Nash, R.: An introduction to convolutional neural networks. CoRR abs\/1511.08458 (2015). http:\/\/dblp.uni-trier.de\/db\/journals\/corr\/corr1511.html#OSheaN15"},{"key":"19_CR59","unstructured":"Prabhakar, P., Rahimi Afzal, Z.: Abstraction based output range analysis for neural networks. Adv. Neural Inf. Process. Syst. 32 (2019)"},{"key":"19_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1007\/978-3-319-24574-4_28","volume-title":"Medical Image Computing and Computer-Assisted Intervention \u2013 MICCAI 2015","author":"O Ronneberger","year":"2015","unstructured":"Ronneberger, O., Fischer, P., Brox, T.: U-Net: convolutional networks for biomedical image segmentation. In: Navab, N., Hornegger, J., Wells, W.M., Frangi, A.F. (eds.) MICCAI 2015. LNCS, vol. 9351, pp. 234\u2013241. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24574-4_28"},{"key":"19_CR61","unstructured":"Rubanova, Y., Chen, R.T.Q., Duvenaud, D.K.: Latent ordinary differential equations for irregularly-sampled time series. In: Wallach, H., Larochelle, H., Beygelzimer, A., d\u2019Alch\u00e9-Buc, F., Fox, E., Garnett, R. (eds.) Advances in Neural Information Processing Systems, vol. 32. Curran Associates, Inc. (2019)"},{"key":"19_CR62","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/978-3-030-81685-8_10","volume-title":"Computer Aided Verification","author":"W Ryou","year":"2021","unstructured":"Ryou, W., Chen, J., Balunovic, M., Singh, G., Dan, A., Vechev, M.: Scalable polyhedral verification of recurrent neural networks. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 225\u2013248. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_10"},{"key":"19_CR63","doi-asserted-by":"publisher","unstructured":"Schilling, C., Forets, M., Guadalupe, S.: Verification of neural-network control systems by integrating Taylor models and zonotopes. In: AAAI, pp. 8169\u20138177. AAAI Press (2022). https:\/\/doi.org\/10.1609\/aaai.v36i7.20790","DOI":"10.1609\/aaai.v36i7.20790"},{"key":"19_CR64","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/978-3-030-81685-8_6","volume-title":"Computer Aided Verification","author":"D Shriver","year":"2021","unstructured":"Shriver, D., Elbaum, S., Dwyer, M.B.: DNNV: a framework for deep neural network verification. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 137\u2013150. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_6"},{"key":"19_CR65","unstructured":"Singh, G., Gehr, T., Mirman, M., P\u00fcschel, M., Vechev, M.: Fast and effective robustness certification. In: Advances in Neural Information Processing Systems, pp. 10825\u201310836 (2018)"},{"key":"19_CR66","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":"19_CR67","unstructured":"Szegedy, C., et al.: Intriguing properties of neural networks. arXiv preprint arXiv:1312.6199 (2013)"},{"key":"19_CR68","unstructured":"The MathWorks, I.: Deep Learning Toolbox Converter for ONNX Model Format. Natick, Massachusetts, United State (2022). https:\/\/www.mathworks.com\/matlabcentral\/fileexchange\/67296-deep-learning-toolbox-converter-for-onnx-model-format"},{"key":"19_CR69","unstructured":"The MathWorks, I.: Deep Learning Toolbox Verification Library. Natick, Massachusetts, United State (2022). https:\/\/www.mathworks.com\/matlabcentral\/fileexchange\/118735-deep-learning-toolbox-verification-library"},{"key":"19_CR70","unstructured":"The MathWorks, I.: Optimization Toolbox. Natick, Massachusetts, United State (2022). https:\/\/www.mathworks.com\/products\/optimization.html"},{"key":"19_CR71","unstructured":"Thoma, M.: A survey of semantic segmentation (2016)"},{"key":"19_CR72","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":"19_CR73","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 (2019)","DOI":"10.1145\/3358230"},{"key":"19_CR74","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) (2023)","DOI":"10.1145\/3575870.3587128"},{"key":"19_CR75","doi-asserted-by":"publisher","unstructured":"Tran, H.D., et al.: Parallelizable reachability analysis algorithms for feed-forward neural networks. In: Proceedings of the 7th International Workshop on Formal Methods in Software Engineering (FormaliSE 2019), pp. 31\u201340. IEEE Press, Piscataway (2019). https:\/\/doi.org\/10.1109\/FormaliSE.2019.00012","DOI":"10.1109\/FormaliSE.2019.00012"},{"key":"19_CR76","doi-asserted-by":"crossref","unstructured":"Tran, H.D., et al.: Parallelizable reachability analysis algorithms for feed-forward neural networks. In: 7th International Conference on Formal Methods in Software Engineering (FormaliSE2019), Montreal, Canada (2019)","DOI":"10.1109\/FormaliSE.2019.00012"},{"key":"19_CR77","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":"19_CR78","doi-asserted-by":"crossref","unstructured":"Tran, H.D., et al.: Verification of piecewise deep neural networks: a star set approach with zonotope pre-filter. Formal Asp. Comput. 33(4), 519\u2013545 (2021)","DOI":"10.1007\/s00165-021-00553-4"},{"key":"19_CR79","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.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 263\u2013286. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_12"},{"key":"19_CR80","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) (2020)","DOI":"10.1007\/978-3-030-53288-8_1"},{"key":"19_CR81","unstructured":"Transformation, N.N.V.M.: https:\/\/github.com\/verivital\/nnvmt"},{"key":"19_CR82","doi-asserted-by":"crossref","unstructured":"Vedaldi, A., Lenc, K.: Matconvnet: convolutional neural networks for matlab. In: Proceedings of the 23rd ACM International Conference on Multimedia, pp. 689\u2013692. ACM (2015)","DOI":"10.1145\/2733373.2807412"},{"key":"19_CR83","unstructured":"Wang, S., Pei, K., Whitehouse, J., Yang, J., Jana, S.: Formal security analysis of neural networks using symbolic intervals. In: 27th $$\\{$$USENIX$$\\}$$ Security Symposium ($$\\{$$USENIX$$\\}$$ Security 2018), pp. 1599\u20131614 (2018)"},{"key":"19_CR84","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":"19_CR85","doi-asserted-by":"crossref","unstructured":"Wu, B., Iandola, F.N., Jin, P.H., Keutzer, K.: Squeezedet: unified, small, low power fully convolutional neural networks for real-time object detection for autonomous driving. In: CVPR Workshops, pp. 446\u2013454 (2017)","DOI":"10.1109\/CVPRW.2017.60"},{"issue":"11","key":"19_CR86","doi-asserted-by":"publisher","first-page":"5777","DOI":"10.1109\/TNNLS.2018.2808470","volume":"29","author":"W Xiang","year":"2018","unstructured":"Xiang, W., Tran, H.D., Johnson, T.T.: Output reachable set estimation and verification for multilayer neural networks. IEEE Trans. Neural Netw. Learn. Syst. 29(11), 5777\u20135783 (2018)","journal-title":"IEEE Trans. Neural Netw. Learn. Syst."},{"key":"19_CR87","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":"19_CR88","doi-asserted-by":"publisher","unstructured":"Yamagishi, J., Veaux, C., MacDonald, K.: Cstr vctk corpus: English multi-speaker corpus for cstr voice cloning toolkit (version 0.92). In: University of Edinburgh. The Centre for Speech Technology Research (CSTR) (2019). https:\/\/doi.org\/10.7488\/ds\/2645","DOI":"10.7488\/ds\/2645"},{"key":"19_CR89","unstructured":"Zeqiri, M., Mueller, M.N., Fischer, M., Vechev, M.: Efficient robustness verification of neural ordinary differential equations. In: The Symbiosis of Deep Learning and Differential Equations II (2022)"},{"key":"19_CR90","unstructured":"Zhang, H., Shinn, M., Gupta, A., Gurfinkel, A., Le, N., Narodytska, N.: Verification of recurrent neural networks for cognitive tasks via reachability analysis. In: ECAI 2020, pp. 1690\u20131697. IOS Press (2020)"}],"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-37703-7_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,26]],"date-time":"2023-08-26T11:06:09Z","timestamp":1693047969000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-37703-7_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031377020","9783031377037"],"references-count":90,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-37703-7_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"18 July 2023","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":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 July 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 July 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"35","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.i-cav.org\/2023\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"hotcrp","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"261","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"67","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}