{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T06:59:05Z","timestamp":1779087545732,"version":"3.51.4"},"reference-count":71,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2024,6,10]],"date-time":"2024-06-10T00:00:00Z","timestamp":1717977600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"French program \u201cInvestissements d\u2019Avenir\u201d"},{"name":"French collaborative project TASV"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2024,7,31]]},"abstract":"<jats:p>\n            Neural networks as a machine learning technique are increasingly deployed in various domains. Despite their performance and their continuous improvement, the deployment of neural networks in safety-critical systems, in particular for autonomous mobility, remains restricted. This is mainly due to the lack of (formal) specifications and verification methods and tools that allow for having sufficient confidence in the behavior of the neural-network-based functions. Recent years have seen neural network verification getting more attention; many verification methods were proposed, yet the practical applicability of these methods to real-world neural network models remains limited. The main challenge of neural network verification methods is related to the computational complexity and the large size of neural networks pertaining to complex functions. As a consequence, applying abstraction methods for neural network verification purposes is seen as a promising mean to cope with such issues. The aim of abstraction is to build an\n            <jats:italic>abstract<\/jats:italic>\n            model by\n            <jats:italic>omitting<\/jats:italic>\n            some irrelevant details or some details that are not highly impacting w.r.t some considered features. Thus, the verification process is made faster and easier while preserving, to some extent, the relevant behavior regarding the properties to be examined on the original model. In this article, we review both the abstraction techniques for activation functions and model size reduction approaches, with a particular focus on the latter. The review primarily discusses the application of abstraction techniques on feed-forward neural networks and explores the potential for applying abstraction to other types of neural networks. Throughout the article, we present the main idea of each approach and then discuss its respective advantages and limitations in detail. Finally, we provide some insights and guidelines to improve the discussed methods.\n          <\/jats:p>","DOI":"10.1145\/3617508","type":"journal-article","created":{"date-parts":[[2023,8,28]],"date-time":"2023-08-28T11:45:52Z","timestamp":1693223152000},"page":"1-19","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["A Review of Abstraction Methods Toward Verifying Neural Networks"],"prefix":"10.1145","volume":"23","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5771-7676","authenticated-orcid":false,"given":"Fateh","family":"Boudardara","sequence":"first","affiliation":[{"name":"Technological Research Institute Railenium, Valenciennes, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2435-014X","authenticated-orcid":false,"given":"Abderraouf","family":"Boussif","sequence":"additional","affiliation":[{"name":"Technological Research Institute Railenium, Valenciennes, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8167-3156","authenticated-orcid":false,"given":"Pierre-Jean","family":"Meyer","sequence":"additional","affiliation":[{"name":"Univ Gustave Eiffel, COSYS-ESTAS, Villeneuve d\u2019Ascq, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1160-7997","authenticated-orcid":false,"given":"Mohamed","family":"Ghazel","sequence":"additional","affiliation":[{"name":"Univ Gustave Eiffel, COSYS-ESTAS, Villeneuve d\u2019Ascq, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,6,10]]},"reference":[{"key":"e_1_3_2_2_2","first-page":"6006","volume-title":"Proceedings of the AAAI Conference on Artificial Intelligence","volume":"33","author":"Akintunde Michael E.","year":"2019","unstructured":"Michael E. Akintunde, Andreea Kevorchian, Alessio Lomuscio, and Edoardo Pirovano. 2019. Verification of RNN-based neural agent-environment systems. In Proceedings of the AAAI Conference on Artificial Intelligence, Vol. 33. 6006\u20136013."},{"key":"e_1_3_2_3_2","doi-asserted-by":"crossref","first-page":"92","DOI":"10.1007\/978-3-030-59152-6_5","volume-title":"International Symposium on Automated Technology for Verification and Analysis","author":"Ashok Pranav","year":"2020","unstructured":"Pranav Ashok, Vahid Hashemi, Jan K\u0159et\u00ednsk\u1ef3, and Stefanie Mohr. 2020. Deepabstract: Neural network abstraction for accelerating verification. In International Symposium on Automated Technology for Verification and Analysis. Springer, 92\u2013107."},{"key":"e_1_3_2_4_2","volume-title":"Handbook of Satisfiability","author":"Biere Armin","year":"2009","unstructured":"Armin Biere, Marijn Heule, and Hans van Maaren. 2009. Handbook of Satisfiability. Vol. 185. IOS Press."},{"key":"e_1_3_2_5_2","article-title":"End to end learning for self-driving cars","author":"Bojarski Mariusz","year":"2016","unstructured":"Mariusz Bojarski, Davide Del Testa, Daniel Dworakowski, Bernhard Firner, Beat Flepp, Prasoon Goyal, Lawrence D. Jackel, Mathew Monfort, Urs Muller, Jiakai Zhang, et\u00a0al. 2016. End to end learning for self-driving cars. arXiv preprint arXiv:1604.07316 (2016).","journal-title":"arXiv preprint arXiv:1604.07316"},{"key":"e_1_3_2_6_2","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1007\/978-3-031-15629-8_5","article-title":"A survey of model learning techniques for recurrent neural networks","author":"Bollig Benedikt","year":"2022","unstructured":"Benedikt Bollig, Martin Leucker, and Daniel Neider. 2022. A survey of model learning techniques for recurrent neural networks. In A Journey from Process Algebra via Timed Automata to Model Learning: Essays Dedicated to Frits Vaandrager on the Occasion of His 60th Birthday. 81\u201397.","journal-title":"A Journey from Process Algebra via Timed Automata to Model Learning: Essays Dedicated to Frits Vaandrager on the Occasion of His 60th Birthday"},{"key":"e_1_3_2_7_2","first-page":"14","volume-title":"The 16th International Conference on Verification and Evaluation of Computer and Communication Systems (VECoS\u201923), Proceedings","author":"Boudardara Fateh","year":"2023","unstructured":"Fateh Boudardara, Abderraouf Boussif, and Mohamed Ghazel. 2023. A sound abstraction method towards efficient neural networks verification. In The 16th International Conference on Verification and Evaluation of Computer and Communication Systems (VECoS\u201923), Proceedings. 14."},{"key":"e_1_3_2_8_2","doi-asserted-by":"crossref","first-page":"330","DOI":"10.1007\/978-3-031-14862-0_24","volume-title":"Computer Safety, Reliability, and Security. SAFECOMP 2022 Workshops: DECSoS, DepDevOps, SASSUR, SENSEI, USDAI, and WAISE, Proceedings","author":"Boudardara Fateh","year":"2022","unstructured":"Fateh Boudardara, Abderraouf Boussif, Pierre-Jean Meyer, and Mohamed Ghazel. 2022. Interval weight-based abstraction for neural network verification. In Computer Safety, Reliability, and Security. SAFECOMP 2022 Workshops: DECSoS, DepDevOps, SASSUR, SENSEI, USDAI, and WAISE, Proceedings. Springer, 330\u2013342."},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/3520142"},{"key":"e_1_3_2_10_2","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1007\/978-3-319-68167-2_18","volume-title":"International Symposium on Automated Technology for Verification and Analysis","author":"Cheng Chih-Hong","year":"2017","unstructured":"Chih-Hong Cheng, Georg N\u00fchrenberg, and Harald Ruess. 2017. Maximum resilience of artificial neural networks. In International Symposium on Automated Technology for Verification and Analysis. Springer, 251\u2013268."},{"key":"e_1_3_2_11_2","article-title":"A survey of model compression and acceleration for deep neural networks","author":"Cheng Yu","year":"2017","unstructured":"Yu Cheng, Duo Wang, Pan Zhou, and Tao Zhang. 2017. A survey of model compression and acceleration for deep neural networks. arXiv preprint arXiv:1710.09282 (2017).","journal-title":"arXiv preprint arXiv:1710.09282"},{"key":"e_1_3_2_12_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-319-10575-8","volume-title":"Handbook of Model Checking","author":"Clarke Edmund M.","year":"2018","unstructured":"Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, Roderick Bloem, et\u00a0al. 2018. Handbook of Model Checking. Vol. 10. Springer."},{"key":"e_1_3_2_13_2","first-page":"238","volume-title":"Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages","author":"Cousot Patrick","year":"1977","unstructured":"Patrick Cousot and Radhia Cousot. 1977. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. 238\u2013252."},{"key":"e_1_3_2_14_2","article-title":"Output range analysis for deep neural networks","author":"Dutta Souradeep","year":"2017","unstructured":"Souradeep Dutta, Susmit Jha, Sriram Sanakaranarayanan, and Ashish Tiwari. 2017. Output range analysis for deep neural networks. arXiv preprint arXiv:1709.09130 (2017).","journal-title":"arXiv preprint arXiv:1709.09130"},{"key":"e_1_3_2_15_2","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1007\/978-3-319-77935-5_9","volume-title":"Proceedings of the 10th NASA Formal Methods","author":"Dutta Souradeep","year":"2018","unstructured":"Souradeep Dutta, Susmit Jha, Sriram Sankaranarayanan, and Ashish Tiwari. 2018. Output range analysis for deep feedforward neural networks. In Proceedings of the 10th NASA Formal Methods. 121\u2013138. 10.1007\/978-3-319-77935-5_9"},{"key":"e_1_3_2_16_2","first-page":"3","volume-title":"UAI","author":"Dvijotham Krishnamurthy","year":"2018","unstructured":"Krishnamurthy Dvijotham, Robert Stanforth, Sven Gowal, Timothy A. Mann, and Pushmeet Kohli. 2018. A dual approach to scalable verification of deep networks. In UAI, Vol. 1. 3."},{"key":"e_1_3_2_17_2","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1007\/978-3-319-68167-2_19","volume-title":"International Symposium on Automated Technology for Verification and Analysis","author":"Ehlers Ruediger","year":"2017","unstructured":"Ruediger Ehlers. 2017. Formal verification of piece-wise linear feed-forward neural networks. In International Symposium on Automated Technology for Verification and Analysis. Springer, 269\u2013286."},{"key":"e_1_3_2_18_2","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1007\/978-3-030-53288-8_3","volume-title":"International Conference on Computer Aided Verification","author":"Elboher Yizhak Yisrael","year":"2020","unstructured":"Yizhak Yisrael Elboher, Justin Gottschlich, and Guy Katz. 2020. An abstraction-based framework for neural network verification. In International Conference on Computer Aided Verification. Springer, 43\u201365."},{"key":"e_1_3_2_19_2","volume-title":"Refactoring: Improving the Design of Existing Code","author":"Fowler Martin","year":"2018","unstructured":"Martin Fowler. 2018. Refactoring: Improving the Design of Existing Code. Addison-Wesley Professional."},{"key":"e_1_3_2_20_2","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1109\/SP.2018.00058","volume-title":"2018 IEEE Symposium on Security and Privacy (SP\u201918)","author":"Gehr Timon","year":"2018","unstructured":"Timon Gehr, Matthew Mirman, Dana Drachsler-Cohen, Petar Tsankov, Swarat Chaudhuri, and Martin Vechev. 2018. Ai2: Safety and robustness certification of neural networks with abstract interpretation. In 2018 IEEE Symposium on Security and Privacy (SP\u201918). IEEE, 3\u201318."},{"key":"e_1_3_2_21_2","doi-asserted-by":"crossref","first-page":"627","DOI":"10.1007\/978-3-642-02658-4_47","volume-title":"International Conference on Computer Aided Verification","author":"Ghorbal Khalil","year":"2009","unstructured":"Khalil Ghorbal, Eric Goubault, and Sylvie Putot. 2009. The zonotope abstract domain taylor1+. In International Conference on Computer Aided Verification. Springer, 627\u2013633."},{"key":"e_1_3_2_22_2","volume-title":"Deep Learning","author":"Goodfellow Ian","year":"2016","unstructured":"Ian Goodfellow, Yoshua Bengio, and Aaron Courville. 2016. Deep Learning. MIT Press."},{"key":"e_1_3_2_23_2","article-title":"Deep compression: Compressing deep neural networks with pruning, trained quantization and Huffman coding","author":"Han Song","year":"2015","unstructured":"Song Han, Huizi Mao, and William J. Dally. 2015. Deep compression: Compressing deep neural networks with pruning, trained quantization and Huffman coding. arXiv preprint arXiv:1510.00149 (2015).","journal-title":"arXiv preprint arXiv:1510.00149"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/3358228"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.cosrev.2020.100270"},{"key":"e_1_3_2_26_2","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/978-3-319-63387-9_1","volume-title":"International Conference on Computer Aided Verification","author":"Huang Xiaowei","year":"2017","unstructured":"Xiaowei Huang, Marta Kwiatkowska, Sen Wang, and Min Wu. 2017. Safety verification of deep neural networks. In International Conference on Computer Aided Verification. Springer, 3\u201329."},{"issue":"1","key":"e_1_3_2_27_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3419742","article-title":"Verifying the safety of autonomous systems with neural network controllers","volume":"20","author":"Ivanov Radoslav","year":"2020","unstructured":"Radoslav Ivanov, Taylor J. Carpenter, James Weimer, Rajeev Alur, George J. Pappas, and Insup Lee. 2020. Verifying the safety of autonomous systems with neural network controllers. ACM Transactions on Embedded Computing Systems (TECS) 20, 1 (2020), 1\u201326.","journal-title":"ACM Transactions on Embedded Computing Systems (TECS)"},{"issue":"5","key":"e_1_3_2_28_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3477023","article-title":"Compositional learning and verification of neural network controllers","volume":"20","author":"Ivanov Radoslav","year":"2021","unstructured":"Radoslav Ivanov, Kishor Jothimurugan, Steve Hsu, Shaan Vaidya, Rajeev Alur, and Osbert Bastani. 2021. Compositional learning and verification of neural network controllers. ACM Transactions on Embedded Computing Systems (TECS) 20, 5s (2021), 1\u201326.","journal-title":"ACM Transactions on Embedded Computing Systems (TECS)"},{"key":"e_1_3_2_29_2","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1007\/978-3-030-59152-6_3","volume-title":"Automated Technology for Verification and Analysis: 18th International Symposium (ATVA\u201920), Proceedings","author":"Jacoby Yuval","year":"2020","unstructured":"Yuval Jacoby, Clark Barrett, and Guy Katz. 2020. Verifying recurrent neural networks using invariant inference. In Automated Technology for Verification and Analysis: 18th International Symposium (ATVA\u201920), Proceedings. Springer, 57\u201374."},{"key":"e_1_3_2_30_2","first-page":"1782","article-title":"Efficient exact verification of binarized neural networks","volume":"33","author":"Jia Kai","year":"2020","unstructured":"Kai Jia and Martin Rinard. 2020. Efficient exact verification of binarized neural networks. Advances in Neural Information Processing Systems 33 (2020), 1782\u20131795.","journal-title":"Advances in Neural Information Processing Systems"},{"key":"e_1_3_2_31_2","first-page":"1","volume-title":"2016 IEEE\/AIAA 35th Digital Avionics Systems Conference (DASC\u201916)","author":"Julian Kyle D.","year":"2016","unstructured":"Kyle D. Julian, Jessica Lopez, Jeffrey S. Brush, Michael P. Owen, and Mykel J. Kochenderfer. 2016. Policy compression for aircraft collision avoidance systems. In 2016 IEEE\/AIAA 35th Digital Avionics Systems Conference (DASC\u201916). IEEE, 1\u201310."},{"key":"e_1_3_2_32_2","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1007\/978-3-319-63387-9_5","volume-title":"International Conference on Computer Aided Verification","author":"Katz Guy","year":"2017","unstructured":"Guy Katz, Clark Barrett, David L. Dill, Kyle Julian, and Mykel J. Kochenderfer. 2017. Reluplex: An efficient SMT solver for verifying deep neural networks. In International Conference on Computer Aided Verification. Springer, 97\u2013117."},{"key":"e_1_3_2_33_2","doi-asserted-by":"crossref","first-page":"443","DOI":"10.1007\/978-3-030-25540-4_26","volume-title":"International Conference on Computer Aided Verification","author":"Katz Guy","year":"2019","unstructured":"Guy Katz, Derek A. Huang, Duligur Ibeling, Kyle Julian, Christopher Lazarus, Rachel Lim, Parth Shah, Shantanu Thakoor, Haoze Wu, Aleksandar Zelji\u0107, et\u00a0al. 2019. The Marabou framework for verification and analysis of deep neural networks. In International Conference on Computer Aided Verification. Springer, 443\u2013452."},{"key":"e_1_3_2_34_2","first-page":"7272","volume-title":"Proceedings of the AAAI Conference on Artificial Intelligence","volume":"36","author":"Lan Jianglin","year":"2022","unstructured":"Jianglin Lan, Yang Zheng, and Alessio Lomuscio. 2022. Tight neural network verification via semidefinite relaxations and linear reformulations. In Proceedings of the AAAI Conference on Artificial Intelligence, Vol. 36. 7272\u20137280."},{"issue":"1","key":"e_1_3_2_35_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0890-5401(91)90030-6","article-title":"Bisimulation through probabilistic testing","volume":"94","author":"Larsen Kim G.","year":"1991","unstructured":"Kim G. Larsen and Arne Skou. 1991. Bisimulation through probabilistic testing. Information and Computation 94, 1 (1991), 1\u201328.","journal-title":"Information and Computation"},{"key":"e_1_3_2_36_2","article-title":"A mixed integer programming approach for verifying properties of binarized neural networks","author":"Lazarus Christopher","year":"2022","unstructured":"Christopher Lazarus and Mykel J. Kochenderfer. 2022. A mixed integer programming approach for verifying properties of binarized neural networks. arXiv preprint arXiv:2203.07078 (2022).","journal-title":"arXiv preprint arXiv:2203.07078"},{"key":"e_1_3_2_37_2","volume-title":"The MNIST Database of Handwritten Digits","author":"LeCun Yann","year":"1998","unstructured":"Yann LeCun. 1998. The MNIST Database of Handwritten Digits."},{"issue":"7553","key":"e_1_3_2_38_2","doi-asserted-by":"crossref","first-page":"436","DOI":"10.1038\/nature14539","article-title":"Deep learning","volume":"521","author":"LeCun Yann","year":"2015","unstructured":"Yann LeCun, Yoshua Bengio, and Geoffrey Hinton. 2015. Deep learning. Nature 521, 7553 (2015), 436\u2013444.","journal-title":"Nature"},{"key":"e_1_3_2_39_2","article-title":"Automated verification of neural networks: Advances, challenges and perspectives","author":"Leofante Francesco","year":"2018","unstructured":"Francesco Leofante, Nina Narodytska, Luca Pulina, and Armando Tacchella. 2018. Automated verification of neural networks: Advances, challenges and perspectives. arXiv preprint arXiv:1805.09938 (2018).","journal-title":"arXiv preprint arXiv:1805.09938"},{"key":"e_1_3_2_40_2","first-page":"296","volume-title":"International Static Analysis Symposium","author":"Li Jianlin","year":"2019","unstructured":"Jianlin Li, Jiangchao Liu, Pengfei Yang, Liqian Chen, Xiaowei Huang, and Lijun Zhang. 2019. Analyzing deep neural networks with symbolic propagation: Towards higher precision and faster verification. In International Static Analysis Symposium. Springer, 296\u2013319."},{"key":"e_1_3_2_41_2","doi-asserted-by":"crossref","first-page":"370","DOI":"10.1016\/j.neucom.2021.07.045","article-title":"Pruning and quantization for deep neural network acceleration: A survey","volume":"461","author":"Liang Tailin","year":"2021","unstructured":"Tailin Liang, John Glossner, Lei Wang, Shaobo Shi, and Xiaotong Zhang. 2021. Pruning and quantization for deep neural network acceleration: A survey. Neurocomputing 461 (2021), 370\u2013403.","journal-title":"Neurocomputing"},{"issue":"3","key":"e_1_3_2_42_2","first-page":"244","article-title":"Algorithms for verifying deep neural networks","volume":"4","author":"Liu Changliu","year":"2021","unstructured":"Changliu Liu, Tomer Arnon, Christopher Lazarus, Christopher Strong, Clark Barrett, Mykel J. Kochenderfer, et\u00a0al. 2021. Algorithms for verifying deep neural networks. Foundations and Trends\u00ae in Optimization 4, 3\u20134 (2021), 244\u2013404.","journal-title":"Foundations and Trends\u00ae in Optimization"},{"key":"e_1_3_2_43_2","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1016\/j.neucom.2016.12.038","article-title":"A survey of deep neural network architectures and their applications","volume":"234","author":"Liu Weibo","year":"2017","unstructured":"Weibo Liu, Zidong Wang, Xiaohui Liu, Nianyin Zeng, Yurong Liu, and Fuad E. Alsaadi. 2017. A survey of deep neural network architectures and their applications. Neurocomputing 234 (2017), 11\u201326.","journal-title":"Neurocomputing"},{"key":"e_1_3_2_44_2","article-title":"An approach to reachability analysis for feed-forward Relu neural networks","author":"Lomuscio Alessio","year":"2017","unstructured":"Alessio Lomuscio and Lalit Maganti. 2017. An approach to reachability analysis for feed-forward Relu neural networks. arXiv preprint arXiv:1706.07351 (2017).","journal-title":"arXiv preprint arXiv:1706.07351"},{"issue":"2","key":"e_1_3_2_45_2","doi-asserted-by":"crossref","first-page":"1088","DOI":"10.1109\/LRA.2018.2795643","article-title":"Dronet: Learning to fly by driving","volume":"3","author":"Loquercio Antonio","year":"2018","unstructured":"Antonio Loquercio, Ana I. Maqueda, Carlos R. Del-Blanco, and Davide Scaramuzza. 2018. Dronet: Learning to fly by driving. IEEE Robotics and Automation Letters 3, 2 (2018), 1088\u20131095.","journal-title":"IEEE Robotics and Automation Letters"},{"key":"e_1_3_2_46_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3498704","article-title":"PRIMA: General and precise neural network certification via scalable convex hull approximations","volume":"6","author":"M\u00fcller Mark Niklas","year":"2022","unstructured":"Mark Niklas M\u00fcller, Gleb Makarchuk, Gagandeep Singh, Markus P\u00fcschel, and Martin Vechev. 2022. PRIMA: General and precise neural network certification via scalable convex hull approximations. Proceedings of the ACM on Programming Languages 6, POPL (2022), 1\u201333.","journal-title":"Proceedings of the ACM on Programming Languages"},{"key":"e_1_3_2_47_2","volume-title":"Proceedings of the AAAI Conference on Artificial Intelligence","volume":"32","author":"Narodytska Nina","year":"2018","unstructured":"Nina Narodytska, Shiva Kasiviswanathan, Leonid Ryzhyk, Mooly Sagiv, and Toby Walsh. 2018. Verifying properties of binarized deep neural networks. In Proceedings of the AAAI Conference on Artificial Intelligence, Vol. 32."},{"key":"e_1_3_2_48_2","doi-asserted-by":"crossref","first-page":"391","DOI":"10.1007\/978-3-031-19992-9_25","volume-title":"Automated Technology for Verification and Analysis: 20th International Symposium (ATVA\u201922), Proceedings","author":"Ostrovsky Matan","year":"2022","unstructured":"Matan Ostrovsky, Clark Barrett, and Guy Katz. 2022. An abstraction-refinement approach to verifying convolutional neural networks. In Automated Technology for Verification and Analysis: 20th International Symposium (ATVA\u201922), Proceedings. Springer, 391\u2013396."},{"key":"e_1_3_2_49_2","doi-asserted-by":"crossref","first-page":"1706","DOI":"10.1016\/j.procs.2018.05.144","article-title":"Application of deep learning for object detection","volume":"132","author":"Pathak Ajeet Ram","year":"2018","unstructured":"Ajeet Ram Pathak, Manjusha Pandey, and Siddharth Rautaray. 2018. Application of deep learning for object detection. Procedia Computer Science 132 (2018), 1706\u20131717.","journal-title":"Procedia Computer Science"},{"key":"e_1_3_2_50_2","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1007\/978-3-030-94583-1_14","volume-title":"Verification, Model Checking, and Abstract Interpretation: 23rd International Conference (VMCAI\u201922), Proceedings","author":"Prabhakar Pavithra","year":"2022","unstructured":"Pavithra Prabhakar. 2022. Bisimulations for neural network reduction. In Verification, Model Checking, and Abstract Interpretation: 23rd International Conference (VMCAI\u201922), Proceedings. Springer, 285\u2013300."},{"key":"e_1_3_2_51_2","article-title":"Abstraction based output range analysis for neural networks","volume":"32","author":"Prabhakar Pavithra","year":"2019","unstructured":"Pavithra Prabhakar and Zahra Rahimi Afzal. 2019. Abstraction based output range analysis for neural networks. Advances in Neural Information Processing Systems 32 (2019).","journal-title":"Advances in Neural Information Processing Systems"},{"key":"e_1_3_2_52_2","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1007\/978-3-642-14295-6_24","volume-title":"International Conference on Computer Aided Verification","author":"Pulina Luca","year":"2010","unstructured":"Luca Pulina and Armando Tacchella. 2010. An abstraction-refinement approach to verification of artificial neural networks. In International Conference on Computer Aided Verification. Springer, 243\u2013257."},{"key":"e_1_3_2_53_2","article-title":"Certified defenses against adversarial examples","author":"Raghunathan Aditi","year":"2018","unstructured":"Aditi Raghunathan, Jacob Steinhardt, and Percy Liang. 2018. Certified defenses against adversarial examples. arXiv preprint arXiv:1801.09344 (2018).","journal-title":"arXiv preprint arXiv:1801.09344"},{"key":"e_1_3_2_54_2","article-title":"Refactoring neural networks for verification","author":"Shriver David","year":"2019","unstructured":"David Shriver, Dong Xu, Sebastian Elbaum, and Matthew B. Dwyer. 2019. Refactoring neural networks for verification. arXiv preprint arXiv:1908.08026 (2019).","journal-title":"arXiv preprint arXiv:1908.08026"},{"key":"e_1_3_2_55_2","volume-title":"Advances in Neural Information Processing Systems","author":"Singh Gagandeep","year":"2019","unstructured":"Gagandeep Singh, Rupanshu Ganvir, Markus P\u00fcschel, and Martin Vechev. 2019. Beyond the single neuron convex barrier for neural network certification. In Advances in Neural Information Processing Systems, H. Wallach, H. Larochelle, A. Beygelzimer, F. d'Alch\u00e9-Buc, E. Fox, and R. Garnett (Eds.), Vol. 32. Curran Associates, Inc."},{"key":"e_1_3_2_56_2","article-title":"Fast and effective robustness certification","volume":"31","author":"Singh Gagandeep","year":"2018","unstructured":"Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus P\u00fcschel, and Martin Vechev. 2018. Fast and effective robustness certification. Advances in Neural Information Processing Systems 31 (2018).","journal-title":"Advances in Neural Information Processing Systems"},{"key":"e_1_3_2_57_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3290354","article-title":"An abstract domain for certifying neural networks","volume":"3","author":"Singh Gagandeep","year":"2019","unstructured":"Gagandeep Singh, Timon Gehr, Markus P\u00fcschel, and Martin Vechev. 2019. An abstract domain for certifying neural networks. Proceedings of the ACM on Programming Languages 3, POPL (2019), 1\u201330.","journal-title":"Proceedings of the ACM on Programming Languages"},{"key":"e_1_3_2_58_2","volume-title":"International Conference on Learning Representations","author":"Singh Gagandeep","year":"2019","unstructured":"Gagandeep Singh, Timon Gehr, Markus P\u00fcschel, and Martin Vechev. 2019. Boosting robustness certification of neural networks. In International Conference on Learning Representations."},{"key":"e_1_3_2_59_2","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1007\/978-3-030-65474-0_4","volume-title":"International Static Analysis Symposium","author":"Sotoudeh Matthew","year":"2020","unstructured":"Matthew Sotoudeh and Aditya V. Thakur. 2020. Abstract neural networks. In International Static Analysis Symposium. Springer, 65\u201388."},{"key":"e_1_3_2_60_2","volume-title":"International Conference on Learning Representations","author":"Tjeng Vincent","year":"2019","unstructured":"Vincent Tjeng, Kai Y. Xiao, and Russ Tedrake. 2019. Evaluating robustness of neural networks with mixed integer programming. In International Conference on Learning Representations. https:\/\/openreview.net\/forum?id=HyGIdiRqtm"},{"key":"e_1_3_2_61_2","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1007\/978-3-030-53288-8_2","volume-title":"International Conference on Computer Aided Verification","author":"Tran Hoang-Dung","year":"2020","unstructured":"Hoang-Dung Tran, Stanley Bak, Weiming Xiang, and Taylor T. Johnson. 2020. Verification of deep convolutional neural networks using imagestars. In International Conference on Computer Aided Verification. Springer, 18\u201342."},{"key":"e_1_3_2_62_2","first-page":"670","volume-title":"International Symposium on Formal Methods","author":"Tran Hoang-Dung","year":"2019","unstructured":"Hoang-Dung Tran, Diago Manzanas Lopez, Patrick Musau, Xiaodong Yang, Luan Viet Nguyen, Weiming Xiang, and Taylor T. Johnson. 2019. Star-based reachability analysis of deep neural networks. In International Symposium on Formal Methods. Springer, 670\u2013686."},{"key":"e_1_3_2_63_2","article-title":"Verification approaches for learning-enabled autonomous cyber-physical systems","author":"Tran Hoang-Dung","year":"2020","unstructured":"Hoang-Dung Tran, Weiming Xiang, and Taylor T. Johnson. 2020. Verification approaches for learning-enabled autonomous cyber-physical systems. IEEE Design & Test (2020).","journal-title":"IEEE Design & Test"},{"key":"e_1_3_2_64_2","doi-asserted-by":"crossref","first-page":"514","DOI":"10.1109\/SYSOSE.2018.8428771","volume-title":"2018 13th Annual Conference on System of Systems Engineering (SoSE\u201918)","author":"Trentesaux Damien","year":"2018","unstructured":"Damien Trentesaux, Rudy Dahyot, Abel Ouedraogo, Diego Arenas, S\u00e9bastien Lefebvre, Walter Sch\u00f6n, Benjamin Lussier, and Hugues Cheritel. 2018. The autonomous train. In 2018 13th Annual Conference on System of Systems Engineering (SoSE\u201918). IEEE, 514\u2013520."},{"key":"e_1_3_2_65_2","article-title":"A review of formal methods applied to machine learning","author":"Urban Caterina","year":"2021","unstructured":"Caterina Urban and Antoine Min\u00e9. 2021. A review of formal methods applied to machine learning. arXiv preprint arXiv:2104.02466 (2021).","journal-title":"arXiv preprint arXiv:2104.02466"},{"key":"e_1_3_2_66_2","article-title":"Efficient formal safety analysis of neural networks","author":"Wang Shiqi","year":"2018","unstructured":"Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. 2018. Efficient formal safety analysis of neural networks. arXiv preprint arXiv:1809.08098 (2018).","journal-title":"arXiv preprint arXiv:1809.08098"},{"key":"e_1_3_2_67_2","first-page":"1599","volume-title":"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 27th USENIX Security Symposium (USENIX Security\u201918). 1599\u20131614."},{"key":"e_1_3_2_68_2","first-page":"5286","volume-title":"International Conference on Machine Learning","author":"Wong Eric","year":"2018","unstructured":"Eric Wong and Zico Kolter. 2018. Provable defenses against adversarial examples via the convex outer adversarial polytope. In International Conference on Machine Learning. PMLR, 5286\u20135295."},{"issue":"5","key":"e_1_3_2_69_2","doi-asserted-by":"crossref","first-page":"1821","DOI":"10.1109\/TNNLS.2020.2991090","article-title":"Reachable set estimation for neural network control systems: A simulation-guided approach","volume":"32","author":"Xiang Weiming","year":"2020","unstructured":"Weiming Xiang, Hoang-Dung Tran, Xiaodong Yang, and Taylor T. Johnson. 2020. Reachable set estimation for neural network control systems: A simulation-guided approach. IEEE Transactions on Neural Networks and Learning Systems 32, 5 (2020), 1821\u20131830.","journal-title":"IEEE Transactions on Neural Networks and Learning Systems"},{"key":"e_1_3_2_70_2","volume-title":"Proceedings of the 33rd International Conference on Software Engineering and Knowledge Engineering (SEKE\u201921)","author":"Xu Jin","year":"2021","unstructured":"Jin Xu, Zishan Li, Miaomiao Zhang, and Bowen Du. 2021. Conv-Reluplex: A verification framework for convolution neural networks. In Proceedings of the 33rd International Conference on Software Engineering and Knowledge Engineering (SEKE\u201921)."},{"issue":"3","key":"e_1_3_2_71_2","doi-asserted-by":"crossref","first-page":"407","DOI":"10.1007\/s00165-021-00548-1","article-title":"Enhancing robustness verification for deep neural networks via symbolic propagation","volume":"33","author":"Yang Pengfei","year":"2021","unstructured":"Pengfei Yang, Jianlin Li, Jiangchao Liu, Cheng-Chao Huang, Renjue Li, Liqian Chen, Xiaowei Huang, and Lijun Zhang. 2021. Enhancing robustness verification for deep neural networks via symbolic propagation. Formal Aspects of Computing 33, 3 (2021), 407\u2013435.","journal-title":"Formal Aspects of Computing"},{"key":"e_1_3_2_72_2","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1016\/j.neucom.2020.11.068","article-title":"PFLU and FPFLU: Two novel non-monotonic activation functions in convolutional neural networks","volume":"429","author":"Zhu Meng","year":"2021","unstructured":"Meng Zhu, Weidong Min, Qi Wang, Song Zou, and Xinhao Chen. 2021. PFLU and FPFLU: Two novel non-monotonic activation functions in convolutional neural networks. Neurocomputing 429 (2021), 110\u2013117.","journal-title":"Neurocomputing"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3617508","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3617508","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:45:58Z","timestamp":1750178758000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3617508"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,10]]},"references-count":71,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2024,7,31]]}},"alternative-id":["10.1145\/3617508"],"URL":"https:\/\/doi.org\/10.1145\/3617508","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"value":"1539-9087","type":"print"},{"value":"1558-3465","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,6,10]]},"assertion":[{"value":"2022-05-17","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-08-07","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-06-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}