{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T05:29:14Z","timestamp":1743139754655,"version":"3.40.3"},"publisher-location":"Cham","reference-count":104,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031757778"},{"type":"electronic","value":"9783031757785"}],"license":[{"start":{"date-parts":[[2024,11,18]],"date-time":"2024-11-18T00:00:00Z","timestamp":1731888000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,11,18]],"date-time":"2024-11-18T00:00:00Z","timestamp":1731888000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-75778-5_3","type":"book-chapter","created":{"date-parts":[[2024,11,17]],"date-time":"2024-11-17T12:09:11Z","timestamp":1731845351000},"page":"39-65","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Literature Review on\u00a0Verification and\u00a0Abstraction of\u00a0Neural Networks Within the\u00a0Formal Methods Community"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6078-4175","authenticated-orcid":false,"given":"Sudeep","family":"Kanav","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8122-2881","authenticated-orcid":false,"given":"Jan","family":"K\u0159et\u00ednsk\u00fd","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0006-6397-3100","authenticated-orcid":false,"given":"Sabine","family":"Rieder","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,11,18]]},"reference":[{"key":"3_CR1","unstructured":"Computing Research and Education Conference Portal. http:\/\/portal.core.edu.au\/conf-ranks\/. Accessed 26 June 2024"},{"key":"3_CR2","doi-asserted-by":"publisher","unstructured":"Afzal, M., Gupta, A., Akshay, S.: Using counterexamples to improve robustness verification in neural networks. In: Proceedings of ATVA, pp. 422\u2013443. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-45329-8_20","DOI":"10.1007\/978-3-031-45329-8_20"},{"key":"3_CR3","doi-asserted-by":"publisher","unstructured":"Amir, G., Wu, H., Barrett, C., Katz, G.: An SMT-based approach for verifying binarized neural networks. In: Proceedings of TACAS, pp. 203\u2013222. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_11","DOI":"10.1007\/978-3-030-72013-1_11"},{"key":"3_CR4","doi-asserted-by":"publisher","unstructured":"Anderson, G., Pailoor, S., Dillig, I., Chaudhuri, S.: Optimization and abstraction: a synergistic approach for analyzing neural network robustness. In: Proceedings of PLDI. ACM (2019). https:\/\/doi.org\/10.1145\/3314221.3314614","DOI":"10.1145\/3314221.3314614"},{"key":"3_CR5","doi-asserted-by":"publisher","unstructured":"Ansaripour, M., Chatterjee, K., Henzinger, T.A., Lechner, M., \u017dikeli\u0107, D.: Learning provably stabilizing neural controllers for discrete-time stochastic systems. In: Proceedings of ATVA, pp. 357\u2013379. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-45329-8_17","DOI":"10.1007\/978-3-031-45329-8_17"},{"key":"3_CR6","doi-asserted-by":"publisher","unstructured":"Ashok, P., Hashemi, V., K\u0159et\u00ednsk\u00fd, J., Mohr, S.: DeepAbstract: neural network abstraction for accelerating verification. In: Proceedings of ATVA, pp. 92\u2013107. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-59152-6_5","DOI":"10.1007\/978-3-030-59152-6_5"},{"key":"3_CR7","doi-asserted-by":"publisher","unstructured":"Azeem, M., Grobelna, M., Kanav, S., K\u0159et\u00ednsk\u1ef3, J., Mohr, S., Rieder, S.: Monitizer: automating design and evaluation of neural network monitors. In: Gurfinkel, A., Ganesh, V. (eds.) Proceedings of CAV. LNCS, vol. 14682, pp. 265\u2013279. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-65630-9_14","DOI":"10.1007\/978-3-031-65630-9_14"},{"key":"3_CR8","doi-asserted-by":"publisher","unstructured":"Bak, S., Dohmen, T., Subramani, K., Trivedi, A., Velasquez, A., Wojciechowski, P.: The octatope abstract domain for verification of neural networks. In: Proceedings of FM, pp. 454\u2013472. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-27481-7_26","DOI":"10.1007\/978-3-031-27481-7_26"},{"key":"3_CR9","doi-asserted-by":"publisher","unstructured":"Bak, S., Tran, H., Hobbs, K., Johnson, T.T.: Improved geometric path enumeration for verifying ReLU neural networks. In: Proceedings of CAV, pp. 66\u201396. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_4","DOI":"10.1007\/978-3-030-53288-8_4"},{"key":"3_CR10","unstructured":"Bak, S., Liu, C., Johnson, T.: The second international verification of neural networks competition (vnn-comp 2021): summary and results. arXiv preprint arXiv:2109.00498 (2021)"},{"key":"3_CR11","doi-asserted-by":"publisher","unstructured":"Banerjee, S., Ghosh, S., Banerjee, A., Mohalik, S.K.: SMT-based modeling and verification of spiking neural networks: a case study. In: Proceedings of VMCAI, pp. 25\u201343. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-24950-1_2","DOI":"10.1007\/978-3-031-24950-1_2"},{"issue":"4","key":"3_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3617508","volume":"23","author":"F Boudardara","year":"2024","unstructured":"Boudardara, F., Boussif, A., Meyer, P.J., Ghazel, M.: A review of abstraction methods toward verifying neural networks. IEEE TECS 23(4), 1\u201319 (2024)","journal-title":"IEEE TECS"},{"key":"3_CR13","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"},{"issue":"3","key":"3_CR14","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/s10009-023-00703-4","volume":"25","author":"C Brix","year":"2023","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). STTT 25(3), 329\u2013339 (2023)","journal-title":"STTT"},{"key":"3_CR15","doi-asserted-by":"publisher","unstructured":"Brucker, A.D., Stell, A.: Verifying feedforward neural networks for classification in Isabelle\/HOL. In: Proceedings of FM, pp. 427\u2013444. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-27481-7_24","DOI":"10.1007\/978-3-031-27481-7_24"},{"issue":"8","key":"3_CR16","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"RE Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Computers 35(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Computers"},{"key":"3_CR17","doi-asserted-by":"publisher","unstructured":"Casadio, M., et al.: Neural Network robustness as a verification property: a principled case study. In: Proceedings of CAV, pp. 219\u2013231. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_11","DOI":"10.1007\/978-3-031-13185-1_11"},{"issue":"1","key":"3_CR18","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1049\/cit2.12028","volume":"6","author":"A Chakraborty","year":"2021","unstructured":"Chakraborty, A., Alam, M., Dey, V., Chattopadhyay, A., Mukhopadhyay, D.: A survey on adversarial attacks and defences. CAAI Trans. Intell. Technol. 6(1), 25\u201345 (2021)","journal-title":"CAAI Trans. Intell. Technol."},{"key":"3_CR19","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Henzinger, T.A., Lechner, M., \u017dikeli\u0107, D.: A learner-verifier framework for neural network controllers and certificates of stochastic systems. In: Proceedings of TACAS, pp. 3\u201325. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_1","DOI":"10.1007\/978-3-031-30823-9_1"},{"key":"3_CR20","doi-asserted-by":"publisher","unstructured":"Chau, C., K\u0159et\u00ednsk\u00fd, J., Mohr, S.: Syntactic vs semantic linear abstraction and refinement of neural networks. In: Proceedings of ATVA, pp. 401\u2013421. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-45329-8_19","DOI":"10.1007\/978-3-031-45329-8_19"},{"key":"3_CR21","doi-asserted-by":"publisher","unstructured":"Chen, L.C., Papandreou, G., Kokkinos, I., Murphy, K., Yuille, A.L.: Deeplab: semantic image segmentation with deep convolutional nets, atrous convolution, and fully connected CRFs. IEEE TPAMI 40(4), 834\u2013848 (2018). https:\/\/doi.org\/10.1109\/TPAMI.2017.2699184","DOI":"10.1109\/TPAMI.2017.2699184"},{"key":"3_CR22","doi-asserted-by":"publisher","unstructured":"Cheng, C., N\u00fchrenberg, G., Ruess, H.: Maximum resilience of artificial neural networks. In: Proceedings of ATVA, pp. 251\u2013268. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68167-2_18","DOI":"10.1007\/978-3-319-68167-2_18"},{"key":"3_CR23","doi-asserted-by":"publisher","unstructured":"Christakis, M., et al.: Automated safety verification of programs invoking neural networks. In: Proceedings of CAV, pp. 201\u2013224. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_9","DOI":"10.1007\/978-3-030-81685-8_9"},{"key":"3_CR24","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for the static analysis of programs by construction or approximation of fixpoints. In: Proceedings of POPL, pp. 238\u2013252. ACM (1977). https:\/\/doi.org\/10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"key":"3_CR25","doi-asserted-by":"publisher","unstructured":"Demarchi, S., Guidotti, D., Pulina, L., Tacchella, A.: Supporting standardization of neural networks verification with vnnlib and coconet. In: Narodytska, N., Amir, G., Katz, G., Isac, O. (eds.) Proceedings of FoMLAS, vol.\u00a016, pp. 47\u201358. Kalpa Publications in Computing. EasyChair (2023). https:\/\/doi.org\/10.29007\/5pdh","DOI":"10.29007\/5pdh"},{"key":"3_CR26","doi-asserted-by":"publisher","unstructured":"Dreossi, T., et al.: VerifAI: a toolkit for the formal design and analysis of artificial intelligence-based systems. In: Proceedings of CAV, pp. 432\u2013442. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_25","DOI":"10.1007\/978-3-030-25540-4_25"},{"key":"3_CR27","doi-asserted-by":"publisher","unstructured":"Ehlers, R.: Formal verification of piece-wise linear feed-forward neural networks. In: Proceedings of ATVA, pp. 269\u2013286. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68167-2_19","DOI":"10.1007\/978-3-319-68167-2_19"},{"key":"3_CR28","doi-asserted-by":"publisher","unstructured":"Elboher, Y.Y., Gottschlich, J., Katz, G.: An abstraction-based framework for neural network verification. In: Proceedings of CAV, pp. 43\u201365. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_3","DOI":"10.1007\/978-3-030-53288-8_3"},{"key":"3_CR29","doi-asserted-by":"publisher","unstructured":"Fan, J., Huang, C., Chen, X., Li, W., Zhu, Q.: ReachNN*: a tool for reachability analysis of neural-network controlled systems. In: Proceedings of ATVA, pp. 537\u2013542. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-59152-6_30","DOI":"10.1007\/978-3-030-59152-6_30"},{"key":"3_CR30","unstructured":"Fazlyab, M., Robey, A., Hassani, H., Morari, M., Pappas, G.: Efficient and accurate estimation of lipschitz constants for deep neural networks. In: Proceedings of NeurIPS, vol. 32 (2019)"},{"key":"3_CR31","doi-asserted-by":"publisher","unstructured":"Fischer, M., Sprecher, C., Dimitrov, D.I., Singh, G., Vechev, M.: Shared certificates for neural network verification. In: Proceedings of CAV, 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":"3_CR32","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: Proceedings of S &P, pp. 3\u201318. IEEE (2018)","DOI":"10.1109\/SP.2018.00058"},{"key":"3_CR33","doi-asserted-by":"publisher","unstructured":"Giacobbe, M., Henzinger, T.A., Lechner, M.: How many bits does it take to quantize your neural network? In: Proceedings of TACAS, pp. 79\u201397. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45237-7_5","DOI":"10.1007\/978-3-030-45237-7_5"},{"key":"3_CR34","doi-asserted-by":"publisher","unstructured":"Gross, D., Jansen, N., P\u00e9rez, G.A., Raaijmakers, S.: Robustness verification for classifier ensembles. In: Proceedings of ATVA, pp. 271\u2013287. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-59152-6_15","DOI":"10.1007\/978-3-030-59152-6_15"},{"key":"3_CR35","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1023\/A:1021039126272","volume":"3","author":"IE Grossmann","year":"2002","unstructured":"Grossmann, I.E.: Review of nonlinear mixed-integer and disjunctive programming techniques. Optim. Eng. 3, 227\u2013252 (2002)","journal-title":"Optim. Eng."},{"key":"3_CR36","doi-asserted-by":"publisher","unstructured":"Guidotti, D., Pulina, L., Tacchella, A.: pyNeVer: a framework for learning and verification of neural networks. In: Proceedings of ATVA, pp. 357\u2013363. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-88885-5_23","DOI":"10.1007\/978-3-030-88885-5_23"},{"key":"3_CR37","doi-asserted-by":"publisher","unstructured":"Guo, X., Zhou, Z., Zhang, Y., Katz, G., Zhang, M.: OccRob: efficient SMT-based occlusion robustness verification of deep neural networks. In: Proceedings of TACAS, pp. 208\u2013226. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_11","DOI":"10.1007\/978-3-031-30823-9_11"},{"key":"3_CR38","unstructured":"Hermenegildo, M.V.: Conferences vs. Journals in CS, what to do? Evolutionary ways forward and the ICLP\/TPLP model. In: Dagstuhl 12452: Publication Culture in Computing Research - Position Papers, vol. 12452 (2012)"},{"key":"3_CR39","doi-asserted-by":"publisher","unstructured":"Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety verification of deep neural networks. In: Proceedings of CAV, pp. 3\u201329. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_1","DOI":"10.1007\/978-3-319-63387-9_1"},{"key":"3_CR40","doi-asserted-by":"crossref","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)","DOI":"10.1016\/j.cosrev.2020.100270"},{"key":"3_CR41","doi-asserted-by":"publisher","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: Proceedings of CAV, pp. 249\u2013262. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_11","DOI":"10.1007\/978-3-030-81685-8_11"},{"key":"3_CR42","doi-asserted-by":"publisher","unstructured":"Jacoby, Y., Barrett, C., Katz, G.: Verifying recurrent neural networks using invariant inference. In: Proceedings of ATVA, pp. 57\u201374. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-59152-6_3","DOI":"10.1007\/978-3-030-59152-6_3"},{"key":"3_CR43","doi-asserted-by":"publisher","unstructured":"Jin, P., Tian, J., Zhi, D., Wen, X., Zhang, M.: Trainify: a CEGAR-driven training and verification framework for safe deep reinforcement learning. In: Proceedings of CAV, pp. 193\u2013218. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_10","DOI":"10.1007\/978-3-031-13185-1_10"},{"key":"3_CR44","doi-asserted-by":"crossref","unstructured":"Julian, K.D., Lopez, J., Brush, J.S., Owen, M.P., Kochenderfer, M.J.: Policy compression for aircraft collision avoidance systems. In: Proceedings of DASC, pp. 1\u201310. IEEE (2016)","DOI":"10.1109\/DASC.2016.7778091"},{"key":"3_CR45","doi-asserted-by":"publisher","unstructured":"Kabaha, A., Drachsler-Cohen, D.: Maximal robust neural network specifications via oracle-guided numerical optimization. In: Proceedings of VMCAI, pp. 203\u2013227. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-24950-1_10","DOI":"10.1007\/978-3-031-24950-1_10"},{"key":"3_CR46","doi-asserted-by":"publisher","unstructured":"Kanav, S., K\u0159et\u00ednsk\u00fd, J., Rieder, S.: Reproduction package for submission \u2018a literature review on verification and abstraction of neural networks\u2019. Zenodo (2024). https:\/\/doi.org\/10.5281\/zenodo.12678718","DOI":"10.5281\/zenodo.12678718"},{"key":"3_CR47","doi-asserted-by":"publisher","unstructured":"Katz, G., Barrett, C., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: an efficient SMT solver for verifying deep neural networks. In: Proceedings of CAV, pp. 97\u2013117. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_5","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"3_CR48","doi-asserted-by":"publisher","unstructured":"Katz, G., et al.: The Marabou framework for verification and analysis of deep neural networks. In: Proceedings of CAV, pp. 443\u2013452. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_26","DOI":"10.1007\/978-3-030-25540-4_26"},{"key":"3_CR49","doi-asserted-by":"publisher","unstructured":"Khedr, H., Ferlez, J., Shoukry, Y.: PEREGRiNN: penalized-relaxation greedy neural network verifier. In: Proceedings of CAV, pp. 287\u2013300. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_13","DOI":"10.1007\/978-3-030-81685-8_13"},{"key":"3_CR50","doi-asserted-by":"publisher","unstructured":"Khmelnitsky, I., et al.: Property-directed verification and robustness certification of recurrent neural networks. In: Proceedings of ATVA, pp. 364\u2013380. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-88885-5_24","DOI":"10.1007\/978-3-030-88885-5_24"},{"key":"3_CR51","unstructured":"Kotha, S., Brix, C., Kolter, J.Z., Dvijotham, K., Zhang, H.: Provably bounding neural network preimages. In: Oh, A., Neumann, T., Globerson, A., Saenko, K., Hardt, M., Levine, S. (eds.) Proceedings of NeurIPS, vol.\u00a036, pp. 80270\u201380290. Curran Associates, Inc. (2023). https:\/\/proceedings.neurips.cc\/paper_files\/paper\/2023\/file\/fe061ec0ae03c5cf5b5323a2b9121bfd-Paper-Conference.pdf"},{"key":"3_CR52","doi-asserted-by":"publisher","unstructured":"Laurel, J., Yang, R., Singh, G., Misailovic, S.: A dual number abstraction for static analysis of Clarke Jacobians. PACMPL 6(POPL), 1\u201330 (2022). https:\/\/doi.org\/10.1145\/3498718","DOI":"10.1145\/3498718"},{"key":"3_CR53","unstructured":"Leofante, F., Narodytska, N., Pulina, L., Tacchella, A.: Automated verification of neural networks: Advances, challenges and perspectives. arXiv preprint arXiv:1805.09938 (2018)"},{"issue":"8","key":"3_CR54","doi-asserted-by":"publisher","first-page":"1283","DOI":"10.3390\/electronics11081283","volume":"11","author":"H Liang","year":"2022","unstructured":"Liang, H., He, E., Zhao, Y., Jia, Z., Li, H.: Adversarial attack and defense: a survey. Electronics 11(8), 1283 (2022)","journal-title":"Electronics"},{"key":"3_CR55","doi-asserted-by":"crossref","unstructured":"Liu, C., Arnon, T., Lazarus, C., Strong, C., Barrett, C., Kochenderfer, M.J.: Algorithms for verifying deep neural networks. Found. Trends\u00ae Optimiz. 4(3-4), 244\u2013404 (2021)","DOI":"10.1561\/2400000035"},{"key":"3_CR56","doi-asserted-by":"publisher","unstructured":"Liu, L., et al.: Deep learning for generic object detection: a survey. IJCV 128(2), 261\u2013318 (2020). https:\/\/doi.org\/10.1007\/s11263-019-01247-4","DOI":"10.1007\/s11263-019-01247-4"},{"key":"3_CR57","doi-asserted-by":"publisher","unstructured":"Lopez, D.M., Choi, S.W., Tran, H., Johnson, T.T.: NNV 2.0: the neural network verification tool. In: Proceedings of CAV, 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":"3_CR58","unstructured":"Meng, M.H., et al.: Adversarial robustness of deep neural networks: a survey from a formal verification perspective. In: IEEE TDSC (2022)"},{"key":"3_CR59","doi-asserted-by":"publisher","unstructured":"Mirman, M., H\u00e4gele, A., Bielik, P., Gehr, T., Vechev, M.: Robustness certification with generative models. In: Proceedings of PLDI. PLDI 2021, ACM (2021). https:\/\/doi.org\/10.1145\/3453483.3454100","DOI":"10.1145\/3453483.3454100"},{"key":"3_CR60","unstructured":"Mishra, R., Gupta, H.P., Dutta, T.: A survey on deep neural network compression: challenges, overview, and solutions. arXiv preprint arXiv:2010.03954 (2020)"},{"key":"3_CR61","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":"3_CR62","doi-asserted-by":"publisher","unstructured":"M\u00fcller, M.N., Fischer, M., Staab, R., Vechev, M.: Abstract interpretation of fixpoint iterators with applications to neural networks. PACMPL 7(PLDI), 786\u2013810 (2023). https:\/\/doi.org\/10.1145\/3591252","DOI":"10.1145\/3591252"},{"key":"3_CR63","doi-asserted-by":"publisher","unstructured":"M\u00fcller, M.N., Makarchuk, G., Singh, G., P\u00fcschel, M., Vechev, M.: PRIMA: general and precise neural network certification via scalable convex hull approximations. PACMPL 6(POPL), 1\u201333 (2022). https:\/\/doi.org\/10.1145\/3498704","DOI":"10.1145\/3498704"},{"key":"3_CR64","unstructured":"Neill, J.O.: An overview of neural network compression. arXiv preprint arXiv:2006.03669 (2020)"},{"key":"3_CR65","doi-asserted-by":"publisher","unstructured":"Paulsen, B., Wang, C.: Example guided synthesis of linear approximations for neural network verification. In: Proceedings of CAV, pp. 149\u2013170. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_8","DOI":"10.1007\/978-3-031-13185-1_8"},{"key":"3_CR66","doi-asserted-by":"publisher","unstructured":"Paulsen, B., Wang, C.: LinSyn: synthesizing tight linear bounds for arbitrary neural network activation functions. In: Proceedings of TACAS, pp. 357\u2013376. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_19","DOI":"10.1007\/978-3-030-99524-9_19"},{"key":"3_CR67","doi-asserted-by":"publisher","unstructured":"Pham, L.H., Sun, J.: Verifying neural networks against backdoor attacks. In: Proceedings of CAV, pp. 171\u2013192. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_9","DOI":"10.1007\/978-3-031-13185-1_9"},{"key":"3_CR68","doi-asserted-by":"crossref","unstructured":"Pulina, L., Tacchella, A.: An abstraction-refinement approach to verification of artificial neural networks. In: Proceedings of CAV, pp. 243\u2013257. Springer, Cham (2010)","DOI":"10.1007\/978-3-642-14295-6_24"},{"key":"3_CR69","doi-asserted-by":"publisher","unstructured":"P\u0103s\u0103reanu, C.S., et al.: Closed-loop analysis of vision-based autonomous systems: a case study. In: Proceedings of CAV, 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":"3_CR70","doi-asserted-by":"publisher","unstructured":"Ryou, W., Chen, J., Balunovic, M., Singh, G., Dan, A., Vechev, M.: Scalable polyhedral verification of recurrent neural networks. In: Proceedings of CAV, pp. 225\u2013248. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_10","DOI":"10.1007\/978-3-030-81685-8_10"},{"key":"3_CR71","unstructured":"Salman, H., Yang, G., Zhang, H., Hsieh, C.J., Zhang, P.: A convex relaxation barrier to tight robustness verification of neural networks. In: Proceedings of NeurIPS, vol. 32, pp. 9835\u20139846 (2019)"},{"key":"3_CR72","doi-asserted-by":"publisher","unstructured":"Seshia, S.A., et al.: Formal specification for deep neural networks. In: Proceedings of ATVA, pp. 20\u201334. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_2","DOI":"10.1007\/978-3-030-01090-4_2"},{"key":"3_CR73","unstructured":"Shi, Z., Jin, Q., Kolter, J.Z., Jana, S., Hsieh, C.J., Zhang, H.: Formal verification for neural networks with general nonlinearities via branch-and-bound. In: Proceedings of WFVML (2023)"},{"key":"3_CR74","doi-asserted-by":"publisher","unstructured":"Shriver, D., Elbaum, S., Dwyer, M.B.: DNNV: a framework for deep neural network verification. In: Proceedings of CAV, pp. 137\u2013150. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_6","DOI":"10.1007\/978-3-030-81685-8_6"},{"key":"3_CR75","doi-asserted-by":"publisher","unstructured":"Singh, G., Gehr, T., P\u00fcschel, M., Vechev, M.: An abstract domain for certifying neural networks. In: PACMPL 3(POPL), 1\u201330 (2019). https:\/\/doi.org\/10.1145\/3290354","DOI":"10.1145\/3290354"},{"key":"3_CR76","unstructured":"Singh, G., Gehr, T., Mirman, M., P\u00fcschel, M., Vechev, M.: Fast and effective robustness certification. In: Proceedings of NeurIPS, vol. 31 (2018)"},{"key":"3_CR77","doi-asserted-by":"publisher","unstructured":"Sun, B., Sun, J., Dai, T., Zhang, L.: Probabilistic verification of neural networks against group fairness. In: Proceedings of FM, pp. 83\u2013102. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-90870-6_5","DOI":"10.1007\/978-3-030-90870-6_5"},{"key":"3_CR78","unstructured":"Szegedy, C., et al.: Intriguing properties of neural networks. arXiv preprint arXiv:1312.6199 (2013)"},{"key":"3_CR79","unstructured":"Tan, M., Le, Q.V.: Efficientnet: rethinking model scaling for convolutional neural networks. arXiv preprint arXiv:1905.11946 (2019)"},{"key":"3_CR80","doi-asserted-by":"publisher","unstructured":"Tran, H., Bak, S., Xiang, W., Johnson, T.T.: Verification of deep convolutional neural networks using ImageStars. In: Proceedings of CAV, pp. 18\u201342. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_2","DOI":"10.1007\/978-3-030-53288-8_2"},{"key":"3_CR81","doi-asserted-by":"publisher","unstructured":"Tran, H., et al.: Star-based reachability analysis of deep neural networks. In: Proceedings of FM, pp. 670\u2013686. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30942-8_39","DOI":"10.1007\/978-3-030-30942-8_39"},{"key":"3_CR82","doi-asserted-by":"publisher","unstructured":"Tran, H., et al.: Robustness verification of semantic segmentation neural networks using relaxed reachability. In: Proceedings of CAV, pp. 263\u2013286. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_12","DOI":"10.1007\/978-3-030-81685-8_12"},{"key":"3_CR83","doi-asserted-by":"publisher","unstructured":"Tran, H., et al.: NNV: the neural network verification tool for deep neural networks and learning-enabled cyber-physical systems. In: Proceedings of CAV, pp. 3\u201317. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_1","DOI":"10.1007\/978-3-030-53288-8_1"},{"key":"3_CR84","doi-asserted-by":"publisher","unstructured":"Ugare, S., Banerjee, D., Misailovic, S., Singh, G.: Incremental verification of neural networks. PACMPL 7(PLDI), 1920\u20131945 (2023). https:\/\/doi.org\/10.1145\/3591299","DOI":"10.1145\/3591299"},{"key":"3_CR85","doi-asserted-by":"publisher","unstructured":"Vardi, M.Y.: Conferences vs. journals in computing research. Commun. ACM 52(5), 5 (2009). https:\/\/doi.org\/10.1145\/1506409.1506410","DOI":"10.1145\/1506409.1506410"},{"key":"3_CR86","doi-asserted-by":"publisher","unstructured":"Vrettas, G., Sanderson, M.: Conferences versus journals in computer science. J. Assoc. Inf. Sci. Technol. 66(12), 2674\u20132684 (2015). https:\/\/doi.org\/10.1002\/asi.23349","DOI":"10.1002\/asi.23349"},{"key":"3_CR87","unstructured":"Wang, S., et al.: Beta-CROWN: efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification. In: Proceedings of NeurIPS, vol. 34 (2021)"},{"key":"3_CR88","doi-asserted-by":"publisher","unstructured":"Wu, H., Zelji\u0107, A., Katz, G., Barrett, C.: Efficient neural network analysis with sum-of-infeasibilities. In: Proceedings of TACAS, pp. 143\u2013163. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_8","DOI":"10.1007\/978-3-030-99524-9_8"},{"key":"3_CR89","unstructured":"Xiang, W., et al.: Verification for machine learning, autonomy, and neural networks survey. arXiv preprint arXiv:1810.01989 (2018)"},{"key":"3_CR90","doi-asserted-by":"publisher","unstructured":"Xu, D., Shriver, D., Dwyer, M.B., Elbaum, S.: Systematic generation of diverse benchmarks for DNN verification. In: Proceedings of CAV, pp. 97\u2013121. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_5","DOI":"10.1007\/978-3-030-53288-8_5"},{"key":"3_CR91","unstructured":"Xu, K., et al.: Automatic perturbation analysis for scalable certified robustness and beyond. In: Proceedings of NeurIPS, vol. 33 (2020)"},{"key":"3_CR92","unstructured":"Xu, K., et al.: Fast and complete: enabling complete neural network verification with rapid and massively parallel incomplete verifiers. In: Proceedings of ICLR (2021). https:\/\/openreview.net\/forum?id=nVZtXBI6LNn"},{"key":"3_CR93","unstructured":"Yang, J., Zhou, K., Li, Y., Liu, Z.: Generalized out-of-distribution detection: a survey. In: IJCV, pp. 1\u201328 (2024)"},{"key":"3_CR94","doi-asserted-by":"publisher","unstructured":"Yang, P., et al.: Improving neural network verification through spurious region guided refinement. In: Proceedings of TACAS, pp. 389\u2013408. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72016-2_21","DOI":"10.1007\/978-3-030-72016-2_21"},{"key":"3_CR95","doi-asserted-by":"publisher","unstructured":"Yang, Z., et al.: An iterative scheme of safe reinforcement learning for nonlinear systems via barrier certificate generation. In: Proceedings of CAV, pp. 467\u2013490. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_22","DOI":"10.1007\/978-3-030-81685-8_22"},{"key":"3_CR96","doi-asserted-by":"publisher","unstructured":"Yellin, D.M., Weiss, G.: Synthesizing context-free grammars from recurrent neural networks. In: Proceedings of TACAS, pp. 351\u2013369. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72016-2_19","DOI":"10.1007\/978-3-030-72016-2_19"},{"key":"3_CR97","unstructured":"Zhang, H., et al.: General cutting planes for bound-propagation-based neural network verification. In: Proceedings of NeurIPS (2022)"},{"key":"3_CR98","unstructured":"Zhang, H., et al.: A branch and bound framework for stronger adversarial attacks of ReLU networks. In: Proceedings of ICML, vol.\u00a0162, pp. 26591\u201326604 (2022)"},{"key":"3_CR99","unstructured":"Zhang, H., Weng, T.W., Chen, P.Y., Hsieh, C.J., Daniel, L.: Efficient neural network robustness certification with general activation functions. In: Proceedings of NeurIPS, vol. 31, pp. 4939\u20134948 (2018). https:\/\/arxiv.org\/pdf\/1811.00866.pdf"},{"key":"3_CR100","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2020.106296","volume":"123","author":"J Zhang","year":"2020","unstructured":"Zhang, J., Li, J.: Testing and verification of neural-network-based safety-critical control software: a systematic literature review. Inf. Softw. Technol. 123, 106296 (2020)","journal-title":"Inf. Softw. Technol."},{"key":"3_CR101","doi-asserted-by":"publisher","unstructured":"Zhang, Y., Song, F., Sun, J.: QEBVerif: quantization error bound verification of neural networks. In: Proceedings of CAV, pp. 413\u2013437. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-37703-7_20","DOI":"10.1007\/978-3-031-37703-7_20"},{"key":"3_CR102","doi-asserted-by":"publisher","unstructured":"Zhang, Y., Zhao, Z., Chen, G., Song, F., Chen, T.: BDD4BNN: a BDD-based quantitative analysis framework for binarized neural networks. In: Proceedings of CAV, pp. 175\u2013200. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_8","DOI":"10.1007\/978-3-030-81685-8_8"},{"key":"3_CR103","doi-asserted-by":"publisher","unstructured":"Zhao, C., Sun, Q., Zhang, C., Tang, Y., Qian, F.: Monocular depth estimation based on deep learning: an overview. Sci. China Technol. Sci. 63(9), 1612\u20131627 (2020). https:\/\/doi.org\/10.1007\/s11431-020-1582-8","DOI":"10.1007\/s11431-020-1582-8"},{"key":"3_CR104","doi-asserted-by":"publisher","unstructured":"Zhong, Y., Ta, Q., Khoo, S.: ARENA: enhancing abstract refinement for neural network verification. In: Proceedings of VMCAI, pp. 366\u2013388. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-24950-1_17","DOI":"10.1007\/978-3-031-24950-1_17"}],"container-title":["Lecture Notes in Computer Science","Principles of Verification: Cycling the Probabilistic Landscape"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-75778-5_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,17]],"date-time":"2024-11-17T13:02:32Z","timestamp":1731848552000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-75778-5_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,18]]},"ISBN":["9783031757778","9783031757785"],"references-count":104,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-75778-5_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,11,18]]},"assertion":[{"value":"18 November 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}