{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:40:11Z","timestamp":1774838411108,"version":"3.50.1"},"reference-count":73,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T00:00:00Z","timestamp":1686009600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,6,6]]},"abstract":"<jats:p>Complete verification of deep neural networks (DNNs) can exactly determine whether the DNN satisfies a desired trustworthy property (e.g., robustness, fairness) on an infinite set of inputs or not. Despite the tremendous progress to improve the scalability of complete verifiers over the years on individual DNNs, they are inherently inefficient when a deployed DNN is updated to improve its inference speed or accuracy. The inefficiency is because the expensive verifier needs to be run from scratch on the updated DNN. To improve efficiency, we propose a new, general framework for incremental and complete DNN verification based on the design of novel theory, data structure, and algorithms. Our contributions implemented in a tool named IVAN yield an overall geometric mean speedup of 2.4x for verifying challenging MNIST and CIFAR10 classifiers and a geometric mean speedup of 3.8x for the ACAS-XU classifiers over the state-of-the-art baselines.<\/jats:p>","DOI":"10.1145\/3591299","type":"journal-article","created":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T20:06:24Z","timestamp":1686081984000},"page":"1920-1945","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":16,"title":["Incremental Verification of Neural Networks"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9088-887X","authenticated-orcid":false,"given":"Shubham","family":"Ugare","sequence":"first","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-0163-9717","authenticated-orcid":false,"given":"Debangshu","family":"Banerjee","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7319-8845","authenticated-orcid":false,"given":"Sasa","family":"Misailovic","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9299-2961","authenticated-orcid":false,"given":"Gagandeep","family":"Singh","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA \/ VMware Research, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,6,6]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3292500.3330701"},{"key":"e_1_2_1_2_1","doi-asserted-by":"crossref","unstructured":"Aws Albarghouthi. 2021. Introduction to Neural Network Verification. verifieddeeplearning.com. arxiv:2109.10317.  http:\/\/verifieddeeplearning.com \t\t\t\t  Aws Albarghouthi. 2021. Introduction to Neural Network Verification. verifieddeeplearning.com. arxiv:2109.10317.  http:\/\/verifieddeeplearning.com","DOI":"10.1561\/9781680839111"},{"key":"e_1_2_1_3_1","unstructured":"Javier Alvarez-Valle Pratik Bhatu Nishanth Chandran Divya Gupta Aditya Nori Aseem Rastogi Mayank Rathee Rahul Sharma and Shubham Ugare. 2020. Secure Medical Image Analysis with CrypTFlow. arxiv:2012.05064. \t\t\t\t  Javier Alvarez-Valle Pratik Bhatu Nishanth Chandran Divya Gupta Aditya Nori Aseem Rastogi Mayank Rathee Rahul Sharma and Shubham Ugare. 2020. Secure Medical Image Analysis with CrypTFlow. arxiv:2012.05064."},{"key":"e_1_2_1_4_1","article-title":"Artificial neural networks in medical diagnosis","volume":"11","author":"Amato Filippo","year":"2013","unstructured":"Filippo Amato , Alberto L\u00f3pez , Eladia Mar\u00eda Pe\u00f1a-M\u00e9ndez , Petr Va\u0148hara , Ale\u0161 Hampl , and Josef Havel . 2013 . Artificial neural networks in medical diagnosis . Journal of Applied Biomedicine , 11 , 2 (2013). Filippo Amato, Alberto L\u00f3pez, Eladia Mar\u00eda Pe\u00f1a-M\u00e9ndez, Petr Va\u0148hara, Ale\u0161 Hampl, and Josef Havel. 2013. Artificial neural networks in medical diagnosis. Journal of Applied Biomedicine, 11, 2 (2013).","journal-title":"Journal of Applied Biomedicine"},{"key":"e_1_2_1_5_1","volume-title":"Proc. Programming Language Design and Implementation (PLDI).","author":"Anderson Greg","year":"2019","unstructured":"Greg Anderson , Shankara Pailoor , Isil Dillig , and Swarat Chaudhuri . 2019 . Optimization and Abstraction: A Synergistic Approach for Analyzing Neural Network Robustness . In Proc. Programming Language Design and Implementation (PLDI). Greg Anderson, Shankara Pailoor, Isil Dillig, and Swarat Chaudhuri. 2019. Optimization and Abstraction: A Synergistic Approach for Analyzing Neural Network Robustness. In Proc. Programming Language Design and Implementation (PLDI)."},{"key":"e_1_2_1_6_1","doi-asserted-by":"crossref","unstructured":"Ross Anderson Joey Huchette Will Ma Christian Tjandraatmadja and Juan Pablo Vielma. 2020. Strong mixed-integer programming formulations for trained neural networks. Mathematical Programming. \t\t\t\t  Ross Anderson Joey Huchette Will Ma Christian Tjandraatmadja and Juan Pablo Vielma. 2020. Strong mixed-integer programming formulations for trained neural networks. Mathematical Programming.","DOI":"10.1007\/978-3-030-17953-3_3"},{"key":"e_1_2_1_7_1","volume-title":"Johnson","author":"Bak Stanley","year":"2021","unstructured":"Stanley Bak , Changliu Liu , and Taylor T . Johnson . 2021 . The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Results. CoRR , abs\/2109.00498 (2021), arXiv:2109.00498. arxiv:2109.00498 Stanley Bak, Changliu Liu, and Taylor T. Johnson. 2021. The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Results. CoRR, abs\/2109.00498 (2021), arXiv:2109.00498. arxiv:2109.00498"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53288-8_4"},{"key":"e_1_2_1_9_1","volume-title":"Adversarial Training and Provable Defenses: Bridging the Gap. In International Conference on Learning Representations. https:\/\/openreview.net\/forum?id=SJxSDxrKDr","author":"Balunovic Mislav","year":"2020","unstructured":"Mislav Balunovic and Martin Vechev . 2020 . Adversarial Training and Provable Defenses: Bridging the Gap. In International Conference on Learning Representations. https:\/\/openreview.net\/forum?id=SJxSDxrKDr Mislav Balunovic and Martin Vechev. 2020. Adversarial Training and Provable Defenses: Bridging the Gap. In International Conference on Learning Representations. https:\/\/openreview.net\/forum?id=SJxSDxrKDr"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491429"},{"key":"e_1_2_1_12_1","volume-title":"Proceedings of Machine Learning and Systems 2020","author":"Blalock Davis W.","year":"2020","unstructured":"Davis W. Blalock , Jose Javier Gonzalez Ortiz , Jonathan Frankle , and John V. Guttag . 2020. What is the State of Neural Network Pruning? In Proceedings of Machine Learning and Systems 2020 , MLSys 2020 , Austin, TX, USA , March 2-4, 2020. Davis W. Blalock, Jose Javier Gonzalez Ortiz, Jonathan Frankle, and John V. Guttag. 2020. What is the State of Neural Network Pruning? In Proceedings of Machine Learning and Systems 2020, MLSys 2020, Austin, TX, USA, March 2-4, 2020."},{"key":"e_1_2_1_13_1","volume-title":"Davide Del Testa","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, and Jiakai Zhang. 2016 . End to end learning for self-driving cars. arXiv preprint arXiv:1604.07316. Mariusz Bojarski, Davide Del Testa, Daniel Dworakowski, Bernhard Firner, Beat Flepp, Prasoon Goyal, Lawrence D Jackel, Mathew Monfort, Urs Muller, and Jiakai Zhang. 2016. End to end learning for self-driving cars. arXiv preprint arXiv:1604.07316."},{"key":"e_1_2_1_14_1","article-title":"Branch and bound for piecewise linear neural network verification","volume":"21","author":"Bunel Rudy","year":"2020","unstructured":"Rudy Bunel , Jingyue Lu , Ilker Turkaslan , Pushmeet Kohli , P Torr , and P Mudigonda . 2020 . Branch and bound for piecewise linear neural network verification . Journal of Machine Learning Research , 21 , 2020 (2020). Rudy Bunel, Jingyue Lu, Ilker Turkaslan, Pushmeet Kohli, P Torr, and P Mudigonda. 2020. Branch and bound for piecewise linear neural network verification. Journal of Machine Learning Research, 21, 2020 (2020).","journal-title":"Journal of Machine Learning Research"},{"key":"e_1_2_1_15_1","volume-title":"An efficient nonconvex reformulation of stagewise convex optimization problems. Advances in Neural Information Processing Systems, 33","author":"Bunel Rudy R","year":"2020","unstructured":"Rudy R Bunel , Oliver Hinder , Srinadh Bhojanapalli , and Krishnamurthy Dvijotham . 2020. An efficient nonconvex reformulation of stagewise convex optimization problems. Advances in Neural Information Processing Systems, 33 ( 2020 ). Rudy R Bunel, Oliver Hinder, Srinadh Bhojanapalli, and Krishnamurthy Dvijotham. 2020. An efficient nonconvex reformulation of stagewise convex optimization problems. Advances in Neural Information Processing Systems, 33 (2020)."},{"key":"e_1_2_1_16_1","volume-title":"Robust Out-of-distribution Detection for Neural Networks. In AAAI-22 Workshop on Adversarial Machine Learning and Beyond.","author":"Chen Jiefeng","year":"2022","unstructured":"Jiefeng Chen , Yixuan Li , Xi Wu , Yingyu Liang , and Somesh Jha . 2022 . Robust Out-of-distribution Detection for Neural Networks. In AAAI-22 Workshop on Adversarial Machine Learning and Beyond. Jiefeng Chen, Yixuan Li, Xi Wu, Yingyu Liang, and Somesh Jha. 2022. Robust Out-of-distribution Detection for Neural Networks. In AAAI-22 Workshop on Adversarial Machine Learning and Beyond."},{"key":"e_1_2_1_17_1","unstructured":"Chih-Hong Cheng and Rongjie Yan. 2020. Continuous Safety Verification of Neural Networks. arxiv:2010.05689. \t\t\t\t  Chih-Hong Cheng and Rongjie Yan. 2020. Continuous Safety Verification of Neural Networks. arxiv:2010.05689."},{"key":"e_1_2_1_18_1","first-page":"157","article-title":"V12. 1: User\u2019s Manual for CPLEX","volume":"46","author":"Cplex IBM ILOG","year":"2009","unstructured":"IBM ILOG Cplex . 2009 . V12. 1: User\u2019s Manual for CPLEX . International Business Machines Corporation , 46 , 53 (2009), 157 . IBM ILOG Cplex. 2009. V12. 1: User\u2019s Manual for CPLEX. International Business Machines Corporation, 46, 53 (2009), 157.","journal-title":"International Business Machines Corporation"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/CVPR.2018.00957"},{"key":"e_1_2_1_21_1","volume-title":"Output Range Analysis for Deep Neural Networks. CoRR, abs\/1709.09130","author":"Dutta Souradeep","year":"2017","unstructured":"Souradeep Dutta , Susmit Jha , Sriram Sankaranarayanan , and Ashish Tiwari . 2017. Output Range Analysis for Deep Neural Networks. CoRR, abs\/1709.09130 ( 2017 ), arXiv:1709.09130. arxiv:1709.09130 Souradeep Dutta, Susmit Jha, Sriram Sankaranarayanan, and Ashish Tiwari. 2017. Output Range Analysis for Deep Neural Networks. CoRR, abs\/1709.09130 (2017), arXiv:1709.09130. arxiv:1709.09130"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-68167-2_19"},{"key":"e_1_2_1_23_1","volume-title":"International Conference on Learning Representations. https:\/\/openreview.net\/forum?id=l_amHf1oaK","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 International Conference on Learning Representations. https:\/\/openreview.net\/forum?id=l_amHf1oaK Claudio Ferrari, Mark Niklas Mueller, Nikola Jovanovi\u0107, and Martin Vechev. 2022. Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound. In International Conference on Learning Representations. https:\/\/openreview.net\/forum?id=l_amHf1oaK"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13185-1_7"},{"key":"e_1_2_1_25_1","volume-title":"Fast Geometric Projections for Local Robustness Certification. In International Conference on Learning Representations. https:\/\/openreview.net\/forum?id=zWy1uxjDdZJ","author":"Fromherz Aymeric","year":"2021","unstructured":"Aymeric Fromherz , Klas Leino , Matt Fredrikson , Bryan Parno , and Corina Pasareanu . 2021 . Fast Geometric Projections for Local Robustness Certification. In International Conference on Learning Representations. https:\/\/openreview.net\/forum?id=zWy1uxjDdZJ Aymeric Fromherz, Klas Leino, Matt Fredrikson, Bryan Parno, and Corina Pasareanu. 2021. Fast Geometric Projections for Local Robustness Certification. In International Conference on Learning Representations. https:\/\/openreview.net\/forum?id=zWy1uxjDdZJ"},{"key":"e_1_2_1_26_1","volume-title":"Sound and Complete Neural Network Repair with Minimality and Locality Guarantees. In International Conference on Learning Representations. https:\/\/openreview.net\/forum?id=xS8AMYiEav3","author":"Fu Feisi","year":"2022","unstructured":"Feisi Fu and Wenchao Li . 2022 . Sound and Complete Neural Network Repair with Minimality and Locality Guarantees. In International Conference on Learning Representations. https:\/\/openreview.net\/forum?id=xS8AMYiEav3 Feisi Fu and Wenchao Li. 2022. Sound and Complete Neural Network Repair with Minimality and Locality Guarantees. In International Conference on Learning Representations. https:\/\/openreview.net\/forum?id=xS8AMYiEav3"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2018.00058"},{"key":"e_1_2_1_28_1","volume-title":"A Survey of Quantization Methods for Efficient Neural Network Inference. CoRR, abs\/2103.13630","author":"Gholami Amir","year":"2021","unstructured":"Amir Gholami , Sehoon Kim , Zhen Dong , Zhewei Yao , Michael W. Mahoney , and Kurt Keutzer . 2021. A Survey of Quantization Methods for Efficient Neural Network Inference. CoRR, abs\/2103.13630 ( 2021 ), arxiv:2103.13630. Amir Gholami, Sehoon Kim, Zhen Dong, Zhewei Yao, Michael W. Mahoney, and Kurt Keutzer. 2021. A Survey of Quantization Methods for Efficient Neural Network Inference. CoRR, abs\/2103.13630 (2021), arxiv:2103.13630."},{"key":"e_1_2_1_29_1","volume-title":"Attribute-Guided Adversarial Training for Robustness to Natural Perturbations","author":"Gokhale Tejas","unstructured":"Tejas Gokhale , Rushil Anirudh , Bhavya Kailkhura , Jayaraman J. Thiagarajan , Chitta Baral , and Yezhou Yang . 2021. Attribute-Guided Adversarial Training for Robustness to Natural Perturbations . In AAAI. AAAI Press , 7574\u20137582. Tejas Gokhale, Rushil Anirudh, Bhavya Kailkhura, Jayaraman J. Thiagarajan, Chitta Baral, and Yezhou Yang. 2021. Attribute-Guided Adversarial Training for Robustness to Natural Perturbations. In AAAI. AAAI Press, 7574\u20137582."},{"key":"e_1_2_1_30_1","unstructured":"Gurobi Optimization LLC. 2018. Gurobi Optimizer Reference Manual. \t\t\t\t  Gurobi Optimization LLC. 2018. Gurobi Optimizer Reference Manual."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2021\/351"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2465449.2465456"},{"key":"e_1_2_1_33_1","volume-title":"Owen","author":"Julian Kyle D.","year":"2018","unstructured":"Kyle D. Julian , Mykel J. Kochenderfer , and Michael P . Owen . 2018 . Deep Neural Network Compression for Aircraft Collision Avoidance Systems. CoRR , abs\/1810.04240 (2018). Kyle D. Julian, Mykel J. Kochenderfer, and Michael P. Owen. 2018. Deep Neural Network Compression for Aircraft Collision Avoidance Systems. CoRR, abs\/1810.04240 (2018)."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.2514\/1.g003724"},{"key":"#cr-split#-e_1_2_1_35_1.1","unstructured":"Anan Kabaha and Dana Drachsler-Cohen. 2022. Boosting Robustness Verification of Semantic Feature Neighborhoods. https:\/\/doi.org\/10.48550\/ARXIV.2209.05446 10.48550\/ARXIV.2209.05446"},{"key":"#cr-split#-e_1_2_1_35_1.2","doi-asserted-by":"crossref","unstructured":"Anan Kabaha and Dana Drachsler-Cohen. 2022. Boosting Robustness Verification of Semantic Feature Neighborhoods. https:\/\/doi.org\/10.48550\/ARXIV.2209.05446","DOI":"10.1007\/978-3-031-22308-2_14"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"e_1_2_1_38_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems: 7th International Conference, TACAS 2001","author":"Lakhnech Yassine","year":"2001","unstructured":"Yassine Lakhnech , Saddek Bensalem , Sergey Berezin , and Sam Owre . 2001 . Incremental Verification by Abstraction . In Tools and Algorithms for the Construction and Analysis of Systems: 7th International Conference, TACAS 2001 , T. Margaria and W. Yi (Eds.). 2031, Springer-Verlag, Genova, Italy. 98\u2013112. Yassine Lakhnech, Saddek Bensalem, Sergey Berezin, and Sam Owre. 2001. Incremental Verification by Abstraction. In Tools and Algorithms for the Construction and Analysis of Systems: 7th International Conference, TACAS 2001, T. Margaria and W. Yi (Eds.). 2031, Springer-Verlag, Genova, Italy. 98\u2013112."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/DAC18074.2021.9586276"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563324"},{"key":"e_1_2_1_41_1","unstructured":"Aleksander Madry Aleksandar Makelov Ludwig Schmidt Dimitris Tsipras and Adrian Vladu. 2017. Towards deep learning models resistant to adversarial attacks. arXiv preprint arXiv:1706.06083. \t\t\t\t  Aleksander Madry Aleksandar Makelov Ludwig Schmidt Dimitris Tsipras and Adrian Vladu. 2017. Towards deep learning models resistant to adversarial attacks. arXiv preprint arXiv:1706.06083."},{"key":"e_1_2_1_42_1","volume-title":"Proc. Machine Learning and Systems (MLSys).","author":"M\u00fcller Christoph","year":"2021","unstructured":"Christoph M\u00fcller , Francois Serre , Gagandeep Singh , Markus P\u00fcschel , and Martin Vechev . 2021 . Scaling Polyhedral Neural Network Verification on GPUs . Proc. Machine Learning and Systems (MLSys). Christoph M\u00fcller, Francois Serre, Gagandeep Singh, Markus P\u00fcschel, and Martin Vechev. 2021. Scaling Polyhedral Neural Network Verification on GPUs. Proc. Machine Learning and Systems (MLSys)."},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209109"},{"key":"e_1_2_1_44_1","volume-title":"Scaling the Convex Barrier with Active Sets. In 9th International Conference on Learning Representations, ICLR 2021","author":"Palma Alessandro De","year":"2021","unstructured":"Alessandro De Palma , Harkirat S. Behl , Rudy R. Bunel , Philip H. S. Torr , and M. Pawan Kumar . 2021 . Scaling the Convex Barrier with Active Sets. In 9th International Conference on Learning Representations, ICLR 2021 , Virtual Event, Austria , May 3-7, 2021 . Alessandro De Palma, Harkirat S. Behl, Rudy R. Bunel, Philip H. S. Torr, and M. Pawan Kumar. 2021. Scaling the Convex Barrier with Active Sets. In 9th International Conference on Learning Representations, ICLR 2021, Virtual Event, Austria, May 3-7, 2021."},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3377811.3380337"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3324884.3416560"},{"key":"e_1_2_1_47_1","volume-title":"Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019","author":"Salman Hadi","year":"2019","unstructured":"Hadi Salman , Greg Yang , Huan Zhang , Cho-Jui Hsieh , and Pengchuan Zhang . 2019 . A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks . In Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019 , NeurIPS 2019, December 8-14, 2019, Vancouver, BC, Canada. Hadi Salman, Greg Yang, Huan Zhang, Cho-Jui Hsieh, and Pengchuan Zhang. 2019. A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks. In Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, NeurIPS 2019, December 8-14, 2019, Vancouver, BC, Canada."},{"key":"e_1_2_1_48_1","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. \t\t\t\t  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."},{"key":"e_1_2_1_49_1","volume-title":"Fast and effective robustness certification. Advances in Neural Information Processing Systems, 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 ). 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)."},{"key":"e_1_2_1_50_1","volume-title":"Proceedings of the ACM on Programming Languages, 3, POPL","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). 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)."},{"key":"e_1_2_1_51_1","volume-title":"Boosting Robustness Certification of Neural Networks. In 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. 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_2_1_52_1","volume-title":"Computing Linear Restrictions of Neural Networks. In Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019","author":"Sotoudeh Matthew","year":"2019","unstructured":"Matthew Sotoudeh and Aditya V. Thakur . 2019 . Computing Linear Restrictions of Neural Networks. In Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019 , NeurIPS 2019 , December 8-14, 2019, Vancouver, BC, Canada. Matthew Sotoudeh and Aditya V. Thakur. 2019. Computing Linear Restrictions of Neural Networks. In Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, NeurIPS 2019, December 8-14, 2019, Vancouver, BC, Canada."},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454044"},{"key":"e_1_2_1_54_1","volume-title":"2nd International Conference on Learning Representations, ICLR 2014, Banff, AB, Canada, April 14-16, 2014, Conference Track Proceedings.","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 2nd International Conference on Learning Representations, ICLR 2014, Banff, AB, Canada, April 14-16, 2014, Conference Track Proceedings. Christian Szegedy, Wojciech Zaremba, Ilya Sutskever, Joan Bruna, Dumitru Erhan, Ian J. Goodfellow, and Rob Fergus. 2014. Intriguing properties of neural networks. In 2nd International Conference on Learning Representations, ICLR 2014, Banff, AB, Canada, April 14-16, 2014, Conference Track Proceedings."},{"key":"e_1_2_1_55_1","volume-title":"Convolutional neural networks for medical image analysis: Full training or fine tuning? IEEE transactions on medical imaging, 35, 5","author":"Tajbakhsh Nima","year":"2016","unstructured":"Nima Tajbakhsh , Jae Y Shin , Suryakanth R Gurudu , R Todd Hurst , Christopher B Kendall , Michael B Gotway , and Jianming Liang . 2016. Convolutional neural networks for medical image analysis: Full training or fine tuning? IEEE transactions on medical imaging, 35, 5 ( 2016 ), 1299\u20131312. Nima Tajbakhsh, Jae Y Shin, Suryakanth R Gurudu, R Todd Hurst, Christopher B Kendall, Michael B Gotway, and Jianming Liang. 2016. Convolutional neural networks for medical image analysis: Full training or fine tuning? IEEE transactions on medical imaging, 35, 5 (2016), 1299\u20131312."},{"key":"e_1_2_1_56_1","unstructured":"TFLite. 2017. TF Lite post-training quantization. https:\/\/www.tensorflow.org\/lite\/performance\/post_training_quantization. \t\t\t\t  TFLite. 2017. TF Lite post-training quantization. https:\/\/www.tensorflow.org\/lite\/performance\/post_training_quantization."},{"key":"e_1_2_1_57_1","unstructured":"Vincent Tjeng Kai Xiao and Russ Tedrake. 2017. Evaluating robustness of neural networks with mixed integer programming. arXiv preprint arXiv:1711.07356. \t\t\t\t  Vincent Tjeng Kai Xiao and Russ Tedrake. 2017. Evaluating robustness of neural networks with mixed integer programming. arXiv preprint arXiv:1711.07356."},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527319"},{"key":"#cr-split#-e_1_2_1_59_1.1","unstructured":"Caterina Urban and Antoine Min\u00e9. 2021. A Review of Formal Methods applied to Machine Learning. https:\/\/doi.org\/10.48550\/ARXIV.2104.02466 10.48550\/ARXIV.2104.02466"},{"key":"#cr-split#-e_1_2_1_59_1.2","unstructured":"Caterina Urban and Antoine Min\u00e9. 2021. A Review of Formal Methods applied to Machine Learning. https:\/\/doi.org\/10.48550\/ARXIV.2104.02466"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/2393596.2393665"},{"key":"e_1_2_1_61_1","unstructured":"Shiqi Wang Kexin Pei Justin Whitehouse Junfeng Yang and Suman Jana. 2018. Efficient formal safety analysis of neural networks. In Advances in Neural Information Processing Systems. \t\t\t\t  Shiqi Wang Kexin Pei Justin Whitehouse Junfeng Yang and Suman Jana. 2018. Efficient formal safety analysis of neural networks. In Advances in Neural Information Processing Systems."},{"key":"e_1_2_1_62_1","unstructured":"Shiqi Wang Huan Zhang Kaidi Xu Xue Lin Suman Jana Cho-Jui Hsieh and J Zico Kolter. 2021. Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Verification. arXiv preprint arXiv:2103.06624. \t\t\t\t  Shiqi Wang Huan Zhang Kaidi Xu Xue Lin Suman Jana Cho-Jui Hsieh and J Zico Kolter. 2021. Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Verification. arXiv preprint arXiv:2103.06624."},{"key":"e_1_2_1_63_1","volume-title":"Online Verification of Deep Neural Networks under Domain or Weight Shift. CoRR, abs\/2106.12732","author":"Wei Tianhao","year":"2021","unstructured":"Tianhao Wei and Changliu Liu . 2021. Online Verification of Deep Neural Networks under Domain or Weight Shift. CoRR, abs\/2106.12732 ( 2021 ), arXiv:2106.12732. arxiv:2106.12732 Tianhao Wei and Changliu Liu. 2021. Online Verification of Deep Neural Networks under Domain or Weight Shift. CoRR, abs\/2106.12732 (2021), arXiv:2106.12732. arxiv:2106.12732"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1186\/s40537-016-0043-6"},{"key":"e_1_2_1_65_1","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. Eric Wong and Zico Kolter. 2018. Provable defenses against adversarial examples via the convex outer adversarial polytope. In International Conference on Machine Learning."},{"key":"e_1_2_1_66_1","volume-title":"Proceedings of the 35th 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 Proceedings of the 35th International Conference on Machine Learning. Eric Wong and Zico Kolter. 2018. Provable Defenses against Adversarial Examples via the Convex Outer Adversarial Polytope. In Proceedings of the 35th International Conference on Machine Learning."},{"key":"e_1_2_1_67_1","unstructured":"Kaidi Xu Zhouxing Shi Huan Zhang Yihan Wang Kai-Wei Chang Minlie Huang Bhavya Kailkhura Xue Lin and Cho-Jui Hsieh. 2020. Automatic Perturbation Analysis for Scalable Certified Robustness and Beyond. \t\t\t\t  Kaidi Xu Zhouxing Shi Huan Zhang Yihan Wang Kai-Wei Chang Minlie Huang Bhavya Kailkhura Xue Lin and Cho-Jui Hsieh. 2020. Automatic Perturbation Analysis for Scalable Certified Robustness and Beyond."},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSM.2009.5306334"},{"key":"e_1_2_1_69_1","unstructured":"Rem Yang Jacob Laurel Sasa Misailovic and Gagandeep Singh. 2022. Provable Defense Against Geometric Transformations. arxiv:2207.11177. \t\t\t\t  Rem Yang Jacob Laurel Sasa Misailovic and Gagandeep Singh. 2022. Provable Defense Against Geometric Transformations. arxiv:2207.11177."},{"key":"e_1_2_1_70_1","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 Advances in Neural Information Processing Systems Alice H. Oh Alekh Agarwal Danielle Belgrave and Kyunghyun Cho (Eds.). https:\/\/openreview.net\/forum?id=5haAJAcofjc \t\t\t\t  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 Advances in Neural Information Processing Systems Alice H. Oh Alekh Agarwal Danielle Belgrave and Kyunghyun Cho (Eds.). https:\/\/openreview.net\/forum?id=5haAJAcofjc"},{"key":"e_1_2_1_71_1","unstructured":"Huan Zhang Tsui-Wei Weng Pin-Yu Chen Cho-Jui Hsieh and Luca Daniel. 2018. Efficient neural network robustness certification with general activation functions. In Advances in neural information processing systems. \t\t\t\t  Huan Zhang Tsui-Wei Weng Pin-Yu Chen Cho-Jui Hsieh and Luca Daniel. 2018. Efficient neural network robustness certification with general activation functions. In Advances in neural information processing systems."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3591299","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3591299","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:47:21Z","timestamp":1750178841000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3591299"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,6,6]]},"references-count":73,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2023,6,6]]}},"alternative-id":["10.1145\/3591299"],"URL":"https:\/\/doi.org\/10.1145\/3591299","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,6,6]]},"assertion":[{"value":"2023-06-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}