{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,12]],"date-time":"2026-03-12T15:25:04Z","timestamp":1773329104682,"version":"3.50.1"},"reference-count":56,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2024,6,3]],"date-time":"2024-06-03T00:00:00Z","timestamp":1717372800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Natural Science Foundation of Guangdong Provinc","award":["No. 2022A1515011458 and No. 2022A1515010880"],"award-info":[{"award-number":["No. 2022A1515011458 and No. 2022A1515010880"]}]},{"DOI":"10.13039\/501100010877","name":"Shenzhen Science and Technology Innovation Commission","doi-asserted-by":"crossref","award":["No. JCYJ20210324094202008"],"award-info":[{"award-number":["No. JCYJ20210324094202008"]}],"id":[{"id":"10.13039\/501100010877","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"crossref","award":["No. 62272315, No. 62072309, No. 62372304, and No. 62002228"],"award-info":[{"award-number":["No. 62272315, No. 62072309, No. 62372304, and No. 62002228"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"name":"CAS Project for Young Scientists in Basic Research","award":["No. YSBR-040"],"award-info":[{"award-number":["No. YSBR-040"]}]},{"name":"ISCAS New Cultivation Project","award":["ISCAS-PYFX-202201"],"award-info":[{"award-number":["ISCAS-PYFX-202201"]}]},{"name":"ISCAS Fundamental Research Project","award":["No. ISCAS-JCZD-202302 and No. ISCAS-JCMS-202308"],"award-info":[{"award-number":["No. ISCAS-JCZD-202302 and No. ISCAS-JCMS-202308"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2024,6,30]]},"abstract":"<jats:p>\n            As a new programming paradigm, deep neural networks (DNNs) have been increasingly deployed in practice, but the lack of robustness hinders their applications in safety-critical domains. While there are techniques for verifying DNNs with formal guarantees, they are limited in scalability and accuracy. In this article, we present a novel counterexample-guided abstraction refinement (CEGAR) approach for scalable and exact verification of DNNs. Specifically, we propose a novel abstraction to break down the size of DNNs by over-approximation. The result of verifying the abstract DNN is conclusive if no spurious counterexample is reported. To eliminate each spurious counterexample introduced by abstraction, we propose a novel counterexample-guided refinement that refines the abstract DNN to exclude the spurious counterexample while still over-approximating the original one, leading to a sound, complete yet efficient CEGAR approach. Our approach is orthogonal to and can be integrated with many existing verification techniques. For demonstration, we implement our approach using two promising tools,\n            <jats:sc>Marabou<\/jats:sc>\n            and\n            <jats:sc>Planet<\/jats:sc>\n            , as the underlying verification engines, and evaluate on widely used benchmarks for three datasets\n            <jats:monospace>ACAS<\/jats:monospace>\n            ,\n            <jats:monospace>Xu<\/jats:monospace>\n            ,\n            <jats:monospace>MNIST<\/jats:monospace>\n            , and\n            <jats:monospace>CIFAR-10<\/jats:monospace>\n            . The results show that our approach can boost their performance by solving more problems in the same time limit, reducing on average 13.4%\u201386.3% verification time of\n            <jats:sc>Marabou<\/jats:sc>\n            on almost all the verification tasks, and reducing on average 8.3%\u201378.0% verification time of\n            <jats:sc>Planet<\/jats:sc>\n            on all the verification tasks. Compared to the most relevant CEGAR-based approach, our approach is 11.6\u201326.6 times faster.\n          <\/jats:p>\n          <jats:p\/>","DOI":"10.1145\/3644387","type":"journal-article","created":{"date-parts":[[2024,2,6]],"date-time":"2024-02-06T07:03:40Z","timestamp":1707203020000},"page":"1-35","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Abstraction and Refinement: Towards Scalable and Exact Verification of Neural Networks"],"prefix":"10.1145","volume":"33","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6725-8167","authenticated-orcid":false,"given":"Jiaxiang","family":"Liu","sequence":"first","affiliation":[{"name":"Shenzhen University, Shenzhen, China"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-1467-4362","authenticated-orcid":false,"given":"Yunhan","family":"Xing","sequence":"additional","affiliation":[{"name":"Shenzhen University, Shenzhen, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6277-2813","authenticated-orcid":false,"given":"Xiaomu","family":"Shi","sequence":"additional","affiliation":[{"name":"State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0581-2679","authenticated-orcid":false,"given":"Fu","family":"Song","sequence":"additional","affiliation":[{"name":"State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6727-440X","authenticated-orcid":false,"given":"Zhiwu","family":"Xu","sequence":"additional","affiliation":[{"name":"Shenzhen University, Shenzhen, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6933-5760","authenticated-orcid":false,"given":"Zhong","family":"Ming","sequence":"additional","affiliation":[{"name":"Shenzhen University &amp; Shenzhen Technology University, Shenzhen, China"}]}],"member":"320","published-online":{"date-parts":[[2024,6,3]]},"reference":[{"key":"e_1_3_2_2_2","unstructured":"Stanley Bak Changliu Liu and Taylor T. Johnson. 2021. The 2nd International Verification of Neural Networks Competition (VNN-COMP\u201921): Summary and Results. CoRR abs\/2109.00498 (2021). https:\/\/arxiv.org\/abs\/2109.00498"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-59152-6_5"},{"key":"e_1_3_2_4_2","unstructured":"Rudy Bunel Ilker Turkaslan Philip H. S. Torr Pushmeet Kohli and M. Pawan Kumar. 2017. Piecewise Linear Neural Network verification: A comparative study. Retrieved from http:\/\/arxiv.org\/abs\/1711.00455"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2017.49"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_15"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512770"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/1014052.1014066"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1016\/b978-0-444-88074-1.50011-1"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-77935-5_9"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-68167-2_19"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53288-8_3"},{"key":"e_1_3_2_14_2","volume-title":"Proceedings of the International Conference on Learning Representations","author":"Ferrari Claudio","year":"2022","unstructured":"Claudio Ferrari, Mark Niklas Mueller, Nikola Jovanovi\u0107, and Martin Vechev. 2022. Complete verification via multi-neuron relaxation guided branch-and-bound. In Proceedings of the International Conference on Learning Representations."},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2018.00058"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_47"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-55754-6_5"},{"key":"e_1_3_2_18_2","volume-title":"Proceedings of the 3rd International Conference on Learning Representations (ICLR\u201915)","author":"Goodfellow Ian J.","year":"2015","unstructured":"Ian J. Goodfellow, Jonathon Shlens, and Christian Szegedy. 2015. Explaining and harnessing adversarial examples. In Proceedings of the 3rd International Conference on Learning Representations (ICLR\u201915)."},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1109\/MSP.2012.2205597"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_1"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.2514\/1.G003724"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","unstructured":"Guy Katz Derek A. Huang Duligur Ibeling Kyle Julian Christopher Lazarus Rachel Lim Parth Shah Shantanu Thakoor Haoze Wu Aleksandar Zeljic David L. Dill Mykel J. Kochenderfer and Clark W. Barrett. 2019. The Marabou framework for verification and analysis of deep neural networks. In Proceedings of the 31st International Conference on Computer Aided Verification (CAV\u201919) Isil Dillig and Serdar Tasiran (Eds.). Springer 443\u2013452. 10.1007\/978-3-030-25540-4_26","DOI":"10.1007\/978-3-030-25540-4_26"},{"key":"e_1_3_2_24_2","unstructured":"Alex Krizhevsky Geoffrey Hinton et\u00a0al. 2009. Learning multiple layers of features from tiny images. Retrieved from https:\/\/www.cs.toronto.edu\/kriz\/learning-features-2009-TR.pdf"},{"key":"e_1_3_2_25_2","volume-title":"Proceedings of the 5th International Conference on Learning Representations (ICLR\u201917)","author":"Kurakin Alexey","year":"2017","unstructured":"Alexey Kurakin, Ian J. Goodfellow, and Samy Bengio. 2017. Adversarial examples in the physical world. In Proceedings of the 5th International Conference on Learning Representations (ICLR\u201917)."},{"key":"e_1_3_2_26_2","volume-title":"ETH Robustness Analyzer for Neural Networks (ERAN)","author":"Lab SRI","year":"2022","unstructured":"SRI Lab. 2022. ETH Robustness Analyzer for Neural Networks (ERAN). Retrieved from https:\/\/github.com\/eth-sri\/eran"},{"key":"e_1_3_2_27_2","unstructured":"Yann LeCun. 1998. The MNIST database of handwritten digits. Retrieved from http:\/\/yann.lecun.com\/exdb\/mnist\/"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1109\/CVPR.2019.01168"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.media.2017.07.005"},{"key":"e_1_3_2_30_2","unstructured":"Alessio Lomuscio and Lalit Maganti. 2017. An approach to reachability analysis for feed-forward ReLU neural networks. Retrieved from http:\/\/arxiv.org\/abs\/1706.07351"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/3238147.3238202"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/3236024.3236082"},{"key":"e_1_3_2_33_2","unstructured":"Wei Ma and Jun Lu. 2017. An equivalence of fully connected layer and convolutional layer. Retrieved from http:\/\/arxiv.org\/abs\/1712.01252"},{"key":"e_1_3_2_34_2","unstructured":"Mark Niklas M\u00fcller Christopher Brix Stanley Bak Changliu Liu and Taylor T. Johnson. 2022. The third international verification of neural networks competition (VNN-COMP 2022): Summary and results. Retrieved from https:\/\/arXiv:2212.10376"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-19992-9_25"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP.2016.36"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/3361566"},{"key":"e_1_3_2_38_2","first-page":"15762","volume-title":"Proceedings of the 32nd Annual Conference on Neural Information Processing Systems (NeurIPS\u201919)","author":"Prabhakar Pavithra","year":"2019","unstructured":"Pavithra Prabhakar and Zahra Rahimi Afzal. 2019. Abstraction based output range analysis for neural networks. In Proceedings of the 32nd Annual Conference on Neural Information Processing Systems (NeurIPS\u201919), Hanna M. Wallach, Hugo Larochelle, Alina Beygelzimer, Florence d\u2019Alch\u00e9-Buc, Emily B. Fox, and Roman Garnett (Eds.). 15762\u201315772."},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_24"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11263-015-0816-y"},{"key":"e_1_3_2_41_2","first-page":"10825","volume-title":"Proceedings of the 31st Annual Conference on Neural Information Processing Systems (NeurIPS\u201918)","author":"Singh Gagandeep","year":"2018","unstructured":"Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus P\u00fcschel, and Martin T. Vechev. 2018. Fast and effective robustness certification. In Proceedings of the 31st Annual Conference on Neural Information Processing Systems (NeurIPS\u201918), Samy Bengio, Hanna M. Wallach, Hugo Larochelle, Kristen Grauman, Nicol\u00f2 Cesa-Bianchi, and Roman Garnett (Eds.). 10825\u201310836."},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290354"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1145\/3238147.3238172"},{"key":"e_1_3_2_44_2","volume-title":"Proceedings of the 2nd International Conference on Learning Representations","author":"Szegedy Christian","year":"2014","unstructured":"Christian Szegedy, Wojciech Zaremba, Ilya Sutskever, Joan Bruna, Dumitru Erhan, Ian J. Goodfellow, and Rob Fergus. 2014. Intriguing properties of neural networks. In Proceedings of the 2nd International Conference on Learning Representations."},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180220"},{"key":"e_1_3_2_46_2","unstructured":"Vincent Tjeng and Russ Tedrake. 2017. Verifying neural networks with mixed integer programming. Retrieved from http:\/\/arxiv.org\/abs\/1711.07356"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30942-8_39"},{"key":"e_1_3_2_48_2","unstructured":"Caterina Urban and Antoine Min\u00e9. 2021. A review of formal methods applied to machine learning. Retrieved from https:\/\/arXiv:2104.02466"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1109\/MIS.2008.34"},{"key":"e_1_3_2_50_2","first-page":"1599","volume-title":"Proceedings of the 27th USENIX Security Symposium (USENIX Security\u201918)","author":"Wang Shiqi","year":"2018","unstructured":"Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. 2018. Formal security analysis of neural networks using symbolic intervals. In Proceedings of the 27th USENIX Security Symposium (USENIX Security\u201918), William Enck and Adrienne Porter Felt (Eds.). USENIX Association, 1599\u20131614. Retrieved from https:\/\/www.usenix.org\/conference\/usenixsecurity18\/presentation\/wang-shiqi"},{"key":"e_1_3_2_51_2","unstructured":"Wikipedia. 2022. Activation Function. Retrieved from https:\/\/en.wikipedia.org\/wiki\/Activation_function"},{"key":"e_1_3_2_52_2","series-title":"Proceedings of Machine Learning Research","first-page":"5283","volume-title":"Proceedings of the 35th International Conference on Machine Learning (ICML\u201918)","volume":"80","author":"Wong Eric","year":"2018","unstructured":"Eric Wong and J. Zico Kolter. 2018. Provable defenses against adversarial examples via the convex outer adversarial polytope. In Proceedings of the 35th International Conference on Machine Learning (ICML\u201918)(Proceedings of Machine Learning Research, Vol. 80), Jennifer G. Dy and Andreas Krause (Eds.). PMLR, 5283\u20135292. Retrieved from http:\/\/proceedings.mlr.press\/v80\/wong18a.html"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72016-2_21"},{"key":"e_1_3_2_54_2","article-title":"General cutting planes for bound-propagation-based neural network verification","author":"Zhang Huan","year":"2022","unstructured":"Huan Zhang, Shiqi Wang, Kaidi Xu, Linyi Li, Bo Li, Suman Jana, Cho-Jui Hsieh, and J. Zico Kolter. 2022. General cutting planes for bound-propagation-based neural network verification. In Proceedings of the Annual Conference on Advances in Neural Information Processing Systems.","journal-title":"Proceedings of the Annual Conference on Advances in Neural Information Processing Systems"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2019.2962027"},{"key":"e_1_3_2_56_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_8"},{"key":"e_1_3_2_57_2","doi-asserted-by":"publisher","DOI":"10.1145\/3551349.3556916"}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3644387","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3644387","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:50:48Z","timestamp":1750287048000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3644387"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,3]]},"references-count":56,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2024,6,30]]}},"alternative-id":["10.1145\/3644387"],"URL":"https:\/\/doi.org\/10.1145\/3644387","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"value":"1049-331X","type":"print"},{"value":"1557-7392","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,6,3]]},"assertion":[{"value":"2023-03-06","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-01-11","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-06-03","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}