{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T06:57:41Z","timestamp":1779087461246,"version":"3.51.4"},"reference-count":92,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T00:00:00Z","timestamp":1718841600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CCF-2238079, CCF-2316233, CNS-2148583"],"award-info":[{"award-number":["CCF-2238079, CCF-2316233, CNS-2148583"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006785","name":"Google","doi-asserted-by":"publisher","award":["Research Scholar Award"],"award-info":[{"award-number":["Research Scholar Award"]}],"id":[{"id":"10.13039\/100006785","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100005144","name":"Qualcomm","doi-asserted-by":"publisher","award":["Innovation Fellowship"],"award-info":[{"award-number":["Innovation Fellowship"]}],"id":[{"id":"10.13039\/100005144","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,6,20]]},"abstract":"<jats:p>We consider the verification of input-relational properties defined over deep neural networks (DNNs) such as robustness against universal adversarial perturbations, monotonicity, etc. Precise verification of these properties requires reasoning about multiple executions of the same DNN. We introduce a novel concept of difference tracking to compute the difference between the outputs of two executions of the same DNN at all layers. We design a new abstract domain, DiffPoly for efficient difference tracking that can scale large DNNs. DiffPoly is equipped with custom abstract transformers for common activation functions (ReLU, Tanh, Sigmoid, etc.) and affine layers and can create precise linear cross-execution constraints. We implement an input-relational verifier for DNNs called RaVeN which uses DiffPoly and linear program formulations to handle a wide range of input-relational properties. Our experimental results on challenging benchmarks show that by leveraging precise linear constraints defined over multiple executions of the DNN, RaVeN gains substantial precision over baselines on a wide range of datasets, networks, and input-relational properties.<\/jats:p>","DOI":"10.1145\/3656377","type":"journal-article","created":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T16:27:20Z","timestamp":1718900840000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Input-Relational Verification of Deep Neural Networks"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0009-0001-0163-9717","authenticated-orcid":false,"given":"Debangshu","family":"Banerjee","sequence":"first","affiliation":[{"name":"University of Illinois at Urbana-Champaign, Urbana, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3079-5652","authenticated-orcid":false,"given":"Changming","family":"Xu","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, Urbana, 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, Urbana, USA"},{"name":"VMware Research, Palo Alto, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,6,20]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"crossref","unstructured":"Aws Albarghouthi. 2021. Introduction to Neural Network Verification. Found. Trends Program. Lang. 7 1-2 (2021) 1\u2013157. https:\/\/doi.org\/10.1561\/2500000051","DOI":"10.1561\/2500000051"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.2478\/v10136-012-0031-x"},{"key":"e_1_3_1_4_2","first-page":"731","article-title":"Optimization and Abstraction: A Synergistic Approach for Analyzing Neural Network Robustness","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). 731\u2013744.","journal-title":"Proc. Programming Language Design and Implementation (PLDI)"},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-27481-7_26"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53288-8_4"},{"key":"e_1_3_1_7_2","unstructured":"Mislav Balunovic Maximilian Baader Gagandeep Singh Timon Gehr and Martin Vechev. 2019. Certifying Geometric Robustness of Neural Networks. In Advances in Neural Information Processing Systems H. Wallach H. Larochelle A. Beygelzimer F. d\u2019Alch\u00e9-Buc E. Fox and R. Garnett (Eds.) Vol. 32. Curran Associates Inc. https:\/\/proceedings neurips.cc\/paper_files\/paper\/2019\/file\/f7fa6aca028e7ff4ef62d75ed025fe76-Paper.pdf"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2004.1310735"},{"key":"e_1_3_1_9_2","unstructured":"Barry Becker and Ronny Kohavi . 1996. Adult. UCI Machine Learning Repository. DOI https:\/\/doi.org\/10.24432\/C5XW20."},{"key":"e_1_3_1_10_2","doi-asserted-by":"crossref","unstructured":"Raven Beutner and Bernd Finkbeiner. 2022. Software Verification of Hyperproperties Beyond k-Safety. In Computer Aided Verification - 34th International Conference CAV 2022 Haifa Israel August 7-10 2022 Proceedings Part I (Lecture Notes in Computer Science Vol. 13371) Sharon Shoham and Yakir Vizel (Eds.). Springer 341\u2013362.","DOI":"10.1007\/978-3-031-13185-1_17"},{"key":"e_1_3_1_11_2","unstructured":"Mariusz Bojarski Davide Del Testa Daniel Dworakowski Bernhard Firner Beat Flepp Prasoon Goyal Lawrence D Jackel Mathew Monfort Urs Muller Jiakai Zhang et al. 2016. End to end learning for self-driving cars. arXiv preprint arXiv:1604.07316 (2016)."},{"key":"e_1_3_1_12_2","doi-asserted-by":"crossref","unstructured":"Laura Bozzelli Adriano Peron and C\u00e9sar S\u00e1nchez. 2021. Asynchronous Extensions of HyperLTL. In 36th Annual ACM\/IEEE Symposium on Logic in Computer Science LICS 2021 Rome Italy June 29 - July 2 2021. IEEE 1\u201313. https:\/\/doi.org\/10.1109\/LICS52264.2021.9470583","DOI":"10.1109\/LICS52264.2021.9470583"},{"key":"e_1_3_1_13_2","unstructured":"Christopher Brix Mark Niklas M\u00fcller Stanley Bak Taylor T Johnson and Changliu Liu. 2023. First three years of the international verification of neural networks competition (VNN-COMP). International fournal on Software Tools for Technology Transfer (2023) 1\u201311."},{"key":"e_1_3_1_14_2","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).","journal-title":"Journal of Machine Learning Research"},{"key":"e_1_3_1_15_2","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)."},{"key":"e_1_3_1_16_2","doi-asserted-by":"crossref","unstructured":"Jacob Burnim and Koushik Sen. 2009. Asserting and Checking Determinism for Multithreaded Programs. In Proceedings of the 7th foint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on The Foundations of Software Engineering (Amsterdam The Netherlands) (ESEC\/FSE \u201809). Association for Computing Machinery New York NY USA 3\u201312. https:\/\/doi.org\/10.1145\/1595696.1595700","DOI":"10.1145\/1595696.1595700"},{"key":"e_1_3_1_17_2","doi-asserted-by":"crossref","unstructured":"Nicholas Carlini and David Wagner. 2017. Towards evaluating the robustness of neural networks. In 2017 ieee symposium on security and privacy (sp). Ieee 39\u201357.","DOI":"10.1109\/SP.2017.49"},{"key":"e_1_3_1_18_2","doi-asserted-by":"crossref","unstructured":"Maria Christakis Hasan Ferit Eniser J\u00f6rg Hoffmann Adish Singla and Valentin W\u00fcstholz. 2022. Specifying and Testing k-Safety Properties for Machine-Learning Models. arXiv preprint arXiv:2206.06054 (2022).","DOI":"10.24963\/ijcai.2023\/528"},{"key":"e_1_3_1_19_2","doi-asserted-by":"crossref","unstructured":"Berkeley R. Churchill Oded Padon Rahul Sharma and Alex Aiken. 2019. Semantic program alignment for equivalence checking. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation PLDI 2019 Phoenix AZ USA June 22\u201326 2019 Kathryn S. McKinley and Kathleen Fisher (Eds.). ACM 1027-1040 https:\/\/doi.org\/10.1145\/3314221.3314596","DOI":"10.1145\/3314221.3314596"},{"key":"e_1_3_1_20_2","unstructured":"Jeremy Cohen Elan Rosenfeld and Zico Kolter. 2019. Certified Adversarial Robustness via Randomized Smoothing. In Proceedings of the 36th International Conference on Machine Learning (Proceedings of Machine Learning Research Vol. 97) Kamalika Chaudhuri and Ruslan Salakhutdinov (Eds.). PMLR 1310\u20131320. https:\/\/proceedings.mlr.press\/v97\/cohen19c.html"},{"key":"e_1_3_1_21_2","doi-asserted-by":"crossref","unstructured":"Patrick Cousot and Nicolas Halbwachs. 1978. Automatic Discovery of Linear Restraints among Variables of a Program In Proceedings of the 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (Tucson Arizona) (POPL \u201878). Association for Computing Machinery New York NY USA 84\u201396. https:\/\/doi.org\/10.1145\/512760.512770","DOI":"10.1145\/512760.512770"},{"key":"e_1_3_1_22_2","doi-asserted-by":"crossref","unstructured":"Hennie Daniels and Marina Velikova. 2010. Monotone and partially monotone neural networks. IEEE Transactions on Neural Networks 21 6 (2010) 906\u2013917.","DOI":"10.1109\/TNN.2010.2044803"},{"key":"e_1_3_1_23_2","unstructured":"Sumanth Dathathri Krishnamurthy Dvijotham Alexey Kurakin Aditi Raghunathan Jonathan Uesato Rudy Bunel Shreya Shankar Jacob Steinhardt Ian J. Goodfellow Percy Liang and Pushmeet Kohli. 2020. Enabling certification of verification-agnostic networks via memory-efficient semidefinite programming. In Advances in Neural Information Processing Systems 33: Annual Conference on Neural Information Processing Systems 2020 NeurIPS 2020 December 6\u201312 2020 virtual Hugo Larochelle Marc\u2019Aurelio Ranzato Raia Hadsell Maria-Florina Balcan and Hsuan-Tien Lin (Eds.). https:\/\/proceedings.neurips.cc\/paper\/2020\/hash\/397d6b4c83c91021fe928a8c4220386b-Abstract.html"},{"key":"e_1_3_1_24_2","unstructured":"D.Banerjee. 2024. RaVeN: v1.1. https:\/\/doi.org\/10.5281\/zenodo. 10807316"},{"key":"e_1_3_1_25_2","unstructured":"Hai Duong Linhan Li ThanhVu Nguyen and Matthew Dwyer. 2023. A DPLL (T) Framework for Verifying Deep Neural Networks. arXiv preprint arXiv:2307.10266 (2023)"},{"key":"e_1_3_1_26_2","doi-asserted-by":"crossref","unstructured":"Ruediger Ehlers. 2017. Formal verification of piece-wise linear feed-forward neural networks. In International Symposium on Automated Technology for Verification and Analysis.","DOI":"10.1007\/978-3-319-68167-2_19"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_18"},{"key":"e_1_3_1_28_2","doi-asserted-by":"crossref","unstructured":"Azadeh Farzan and Anthony Vandikas. 2019. Automated Hypersafety Verification. In Computer Aided Verification 31st International Conference CAV 2019 New York City NY USA July 15-18 2019 Proceedings Part I (Lecture Notes in Computer Science Vol. 11561) Isil Dillig and Serdar Tasiran (Eds.). Springer 200\u2013218. https:\/\/doi.org\/10.1007\/978-3030-25540-4_11","DOI":"10.1007\/978-3-030-25540-4_11"},{"key":"e_1_3_1_29_2","unstructured":"Claudio Ferrari Mark Niklas Mueller Nikola Jovanovi? and Martin Vechev. 2022. Complete Verification via MultiNeuron Relaxation Guided Branch-and-Bound. In International Conference on Learning Representations. https:\/\/openreview.net\/forum?id=1_amHf1oaK"},{"key":"e_1_3_1_30_2","doi-asserted-by":"crossref","unstructured":"Bernd Finkbeiner Markus N. Rabe and C\u00e9sar S\u00e1nchez. 2015. Algorithms for Model Checking HyperLTL and HyperCTL . In Computer Aided Verification - 27th International Conference CAV 2015 San Francisco CA USA July 18-24 2015 Proceedings Part I (Lecture Notes in Computer Science Vol. 9206) Daniel Kroening and Corina S. Pasareanu (Eds.). Springer 30\u201348. https:\/\/doi.org\/10.1007\/978-3-319-21690-4_3","DOI":"10.1007\/978-3-319-21690-4_3"},{"key":"e_1_3_1_31_2","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"},{"key":"e_1_3_1_32_2","doi-asserted-by":"crossref","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).","DOI":"10.1109\/SP.2018.00058"},{"key":"e_1_3_1_33_2","unstructured":"Chuqin Geng Nham Le Xiaojie Xu Zhaoyue Wang Arie Gurfinkel and Xujie Si. 2023. Towards reliable neural specifications. In International Conference on Machine Learning. PMLR 11196-11212."},{"key":"e_1_3_1_34_2","unstructured":"Ian J Goodfellow Jonathon Shlens and Christian Szegedy. 2014. Explaining and harnessing adversarial examples. arXiv preprint arXiv:1412.6572 (2014)."},{"key":"e_1_3_1_35_2","unstructured":"Akhil Gupta Naman Shukla Lavanya Marla Arinbj\u00f6rn Kolbeinsson and Kartik Yellepeddi. 2019. How to incorporate monotonicity in deep networks while preserving flexibility? arXiv preprint arXiv:1909.10662 (2019)"},{"key":"e_1_3_1_36_2","unstructured":"Gurobi Optimization LLC. 2018. Gurobi Optimizer Reference Manual."},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","DOI":"10.1002\/j.1538-7305.1950.tb00463.x"},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","DOI":"10.1016\/0095-0696(78)90006-2"},{"key":"e_1_3_1_39_2","doi-asserted-by":"crossref","unstructured":"Anan Kabaha and Dana Drachsler-Cohen. 2022. Boosting Robustness Verification of Semantic Feature Neighborhoods. In Static Analysis - 29th International Symposium SAS 2022 Auckland New Zealand December 5-7 2022 Proceedings (Lecture Notes in Computer Science Vol. 13790) Gagandeep Singh and Caterina Urban (Eds.). Springer 299\u2013324 https:\/\/doi.org\/10.1007\/978-3-031-22308-2_14","DOI":"10.1007\/978-3-031-22308-2_14"},{"key":"e_1_3_1_40_2","doi-asserted-by":"crossref","unstructured":"Guy Katz Derek Huang Duligur Ibeling Kyle Julian Christopher Lazarus Rachel Lim Parth Shah Shantanu Thakoor Haoze Wu Aleksandar Zelji? David Dill Mykel Kochenderfer and Clark Barrett. 2019. The Marabou Framework for Verification and Analysis of Deep Neural Networks. 443\u2013452.","DOI":"10.1007\/978-3-030-25540-4_26"},{"key":"e_1_3_1_41_2","doi-asserted-by":"crossref","unstructured":"Haitham Khedr and Yasser Shoukry. 2023. CertiFair: A Framework for Certified Global Fairness of Neural Networks. Proceedings of the AAAI Conference on Artificial Intelligence 37 7 (Jun. 2023) 8237\u20138245.","DOI":"10.1609\/aaai.v37i7.25994"},{"key":"e_1_3_1_42_2","doi-asserted-by":"crossref","unstructured":"M\u00e1t\u00e9 Kov\u00e1cs Helmut Seidl and Bernd Finkbeiner. 2013. Relational abstract interpretation for the verification of 2-hypersafety properties. In 2013 ACM SIGSAC Conference on Computer and Communications Security CCS\u201913 Berlin Germany November 4\u20138 2013 Ahmad-Reza Sadeghi Virgil D. Gligor and Moti Yung (Eds.). ACM 211-222 https:\/\/doi.org\/10.1145\/2508859.2516721","DOI":"10.1145\/2508859.2516721"},{"key":"e_1_3_1_43_2","unstructured":"Alex Krizhevsky. 2009. Learning Multiple Layers of Features from Tiny Images. (2009)."},{"key":"e_1_3_1_44_2","doi-asserted-by":"crossref","unstructured":"Jianglin Lan Yang Zheng and Alessio Lomuscio. 2022. Tight Neural Network Verification via Semidefinite Relaxations and Linear Reformulations. In Thirty-Sixth AAAI Conference on Artificial Intelligence AAAI 2022 Thirty-Fourth Conference on Innovative Applications of Artificial Intelligence IAAI 2022 The Twelveth Symposium on Educational Advances in Artificial Intelligence EAAI 2022 Virtual Event February 22 - March 1 2022. AAAI Press 7272-7280 https:\/\/ojs.aaai.org\/index.php\/AAAI\/article\/view\/20689","DOI":"10.1609\/aaai.v36i7.20689"},{"key":"e_1_3_1_45_2","doi-asserted-by":"crossref","unstructured":"Jacob Laurel Siyuan Brant Qian Gagandeep Singh and Sasa Misailovic. 2023. Synthesizing precise static analyzers for automatic differentiation. Proceedings of the ACM on Programming Languages 7 OOPSLA2 (2023) 1964-1992.","DOI":"10.1145\/3622867"},{"key":"e_1_3_1_46_2","unstructured":"Yann LeCun Bernhard E. Boser John S. Denker Donnie Henderson Richard E. Howard Wayne E. Hubbard and Lawrence D. Jackel. 1989. Handwritten Digit Recognition with a Back-Propagation Network. In NIPS. 396\u2013404."},{"key":"e_1_3_1_47_2","first-page":"11908","volume-title":"Proc. Neural Information Processing Systems (NeurIPS)","author":"Li Juncheng","year":"2019","unstructured":"Juncheng Li, Shuhui Qu, Xinjian Li, Joseph Szurley, J. Zico Kolter, and Florian Metze. 2019. Adversarial Music: Real world Audio Adversary against Wake-word Detection System. In Proc. Neural Information Processing Systems (NeurIPS) 11908\u201311918."},{"key":"e_1_3_1_48_2","first-page":"3896","volume-title":"Proc. International Conference on Machine Learning, ICML","author":"Li Juncheng","year":"2019","unstructured":"Juncheng Li, Frank R. Schmidt, and J. Zico Kolter. 2019. Adversarial camera stickers: A physical camera-based attack on deep learning systems. In Proc. International Conference on Machine Learning, ICML, Vol. 97. 3896\u20133904."},{"key":"e_1_3_1_49_2","unstructured":"Xingchao Liu Xing Han Na Zhang and Qiang Liu. 2020. Certified monotonic neural networks. Advances in Neural Information Processing Systems 33 (2020) 15427\u201315438."},{"key":"e_1_3_1_50_2","unstructured":"Zikun Liu Changming Xu Emerson Sie Gagandeep Singh and Deepak Vasisht. 2023. Exploring Practical Vulnerabilities of Machine Learning-based Wireless Systems. In 20th USENIX Symposium on Networked Systems Design and Implementation NSDI 2023 Boston MA April 17\u201319 2023. USENIX Association 1801-1817."},{"key":"e_1_3_1_51_2","unstructured":"Aleksander Madry Aleksandar Makelov Ludwig Schmidt Dimitris Tsipras and Adrian Vladu. 2018. Towards Deep Learning Models Resistant to Adversarial Attacks. In International Conference on Learning Representations. https:\/\/openreview.net\/forum?id=rJzIBfZAb"},{"key":"e_1_3_1_52_2","doi-asserted-by":"crossref","unstructured":"Antoine Min\u00e9. 2001. A new numerical abstract domain based on difference-bound matrices. In Programs as Data Objects: Second Symposium PADO2001 Aarhus Denmark May 21-23 2001 Proceedings. Springer 155\u2013172.","DOI":"10.1007\/3-540-44978-7_10"},{"key":"e_1_3_1_53_2","first-page":"3578","volume-title":"Proc. International Conference on Machine Learning (ICML)","author":"Mirman Matthew","year":"2018","unstructured":"Matthew Mirman, Timon Gehr, and Martin Vechev. 2018. Differentiable abstract interpretation for provably robust neural networks. In Proc. International Conference on Machine Learning (ICML). 3578\u20133586"},{"key":"e_1_3_1_54_2","unstructured":"Matthew Mirman Timon Gehr and Martin Vechev. 2018. Differentiable Abstract Interpretation for Provably Robust Neural Networks. In Proceedings of the 35th International Conference on Machine Learning (Proceedings of Machine Learning Research Vol. 80) Jennifer Dy and Andreas Krause (Eds.). PMLR 3578-3586. https:\/\/proceedings.mlr.press\/v80\/mirman18b.html"},{"key":"e_1_3_1_55_2","doi-asserted-by":"crossref","unstructured":"Seyed-Mohsen Moosavi-Dezfooli Alhussein Fawzi Omar Fawzi and Pascal Frossard. 2017. Universal adversarial perturbations. In Proceedings of the IEEE conference on computer vision and pattern recognition. 1765-1773.","DOI":"10.1109\/CVPR.2017.17"},{"key":"e_1_3_1_56_2","unstructured":"Mark Niklas M\u00fcller Franziska Eckert Marc Fischer and Martin T. Vechev. 2023. Certified Training: Small Boxes are All You Need. In The Eleventh International Conference on Learning Representations ICLR 2023 Kigali Rwanda May 1\u20135 2023. OpenReview.net. https:\/\/openreview.net\/pdf?id=7oFuxtJtUMH"},{"key":"e_1_3_1_57_2","doi-asserted-by":"crossref","unstructured":"Satoshi Munakata Caterina Urban Haruki Yokoyama Koji Yamamoto and Kazuki Munakata. 2023. Verifying Attention Robustness of Deep Neural Networks Against Semantic Perturbations. In NASA Formal Methods - 15th International Symposium NFM 2023 Houston TX USA May 16-18 2023 Proceedings (Lecture Notes in Computer Science Vol. 13903) Kristin Yvonne Rozier and Swarat Chaudhuri (Eds.). Springer 37\u201361. https:\/\/doi.org\/10.1007\/978-3-031-33170-1_3","DOI":"10.1007\/978-3-031-33170-1_3"},{"key":"e_1_3_1_58_2","unstructured":"Alessandro De Palma Harkirat S. Behl Rudy 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\u20137 2021. OpenReview.net. https:\/\/openreview.net\/forum?id=uQfOy7LrlTR"},{"key":"e_1_3_1_59_2","doi-asserted-by":"crossref","unstructured":"Brandon Paulsen Jingbo Wang and Chao Wang. 2020. ReluDiff: Differential Verification of Deep Neural Networks. In Proceedings of the ACM\/IEEE 42nd International Conference on Software Engineering (Seoul South Korea) (ICSE \u201820). Association for Computing Machinery New York NY USA 714\u2013726. https:\/\/doi.org\/10.1145\/3377811.3380337","DOI":"10.1145\/3377811.3380337"},{"key":"e_1_3_1_60_2","doi-asserted-by":"crossref","unstructured":"Brandon Paulsen Jingbo Wang Jiawei Wang and Chao Wang. 2021. NeuroDiff: Scalable Differential Verification of Neural Networks Using Fine-Grained Approximation. In Proceedings of the 35th IEEE\/ACM International Conference on Automated Software Engineering (Virtual Event Australia) (ASE \u201820). Association for Computing Machinery New York NY USA 784\u2013796. https:\/\/doi.org\/10.1145\/3324884.3416560","DOI":"10.1145\/3324884.3416560"},{"key":"e_1_3_1_61_2","unstructured":"Yannik Potdevin Dirk Nowotka and Vijay Ganesh. 2019. An empirical investigation of randomized defenses against adversarial attacks. arXiv preprint arXiv:1909.05580 (2019)."},{"key":"e_1_3_1_62_2","doi-asserted-by":"crossref","unstructured":"Rob Potharst and Adrianus Johannes Feelders. 2002. Classification trees for problems with monotonicity constraints. ACM SIGKDD Explorations Newsletter 4 1 (2002) 1\u201310.","DOI":"10.1145\/568574.568577"},{"key":"e_1_3_1_63_2","unstructured":"Chongli Qin Krishnamurthy (Dj) Dvijotham Brendan O\u2019Donoghue Rudy Bunel Robert Stanforth Sven Gowal Jonathan Uesato Grzegorz Swirszcz and Pushmeet Kohli. 2019. Verification of Non-Linear Specifications for Neural Networks. In International Conference on Learning Representations. https:\/\/openreview.net\/forum?id=HyeFAsRctQ"},{"key":"e_1_3_1_64_2","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\u201314 2019 Vancouver BC Canada."},{"key":"e_1_3_1_65_2","unstructured":"Joseph Scott Guanting Pan Elias B. Khalil and Vijay Ganesh. 2022. Goose: A Meta-Solver for Deep Neural Network Verification. In Proceedings of the 20th Internal Workshop on Satisfiability Modulo Theories co-located with the 11th International foint Conference on Automated Reasoning (IFCAR 2022) part of the 8th Federated Logic Conference (FLoC 2022) Haifa Israel August 11\u201312 2022 (CEUR Workshop Proceedings Vol. 3185) David D\u00e9harbe and Antti E. J. Hyv\u00e4rinen (Eds.). CEUR-WS.org 99-113. https:\/\/ceur-ws.org\/Vol-3185\/extended678.pdf"},{"key":"e_1_3_1_66_2","doi-asserted-by":"crossref","unstructured":"Ron Shemer Arie Gurfinkel Sharon Shoham and Yakir Vizel. 2019. Property Directed Self Composition. In Computer Aided Verification - 31st International Conference CAV 2019 New York City NY USA July 15-18 2019 Proceedings Part I (Lecture Notes in Computer Science Vol. 11561) Isil Dillig and Serdar Tasiran (Eds.). Springer 161\u2013179. https:\/\/doi.org\/10.1007\/978-3-030-25540-4_9","DOI":"10.1007\/978-3-030-25540-4_9"},{"key":"e_1_3_1_67_2","unstructured":"Zhouxing Shi Yihan Wang Huan Zhang J Zico Kolter and Cho-Jui Hsieh. 2022. Efficiently computing local lipschitz constants of neural networks via bound propagation. Advances in Neural Information Processing Systems 35 (2022) 2350-2364."},{"key":"e_1_3_1_68_2","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."},{"key":"e_1_3_1_69_2","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)."},{"key":"e_1_3_1_70_2","doi-asserted-by":"crossref","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).","DOI":"10.1145\/3290354"},{"key":"e_1_3_1_71_2","unstructured":"Gagandeep Singh Timon Gehr Markus P\u00fcschel and Martin Vechev. 2019. Robustness Certification with Refinement. In International Conference on Learning Representations. https:\/\/openreview.net\/forum?id=HJgeEh09KQ"},{"key":"e_1_3_1_72_2","doi-asserted-by":"crossref","unstructured":"Matthew Sotoudeh Zhe Tao and Aditya V Thakur. 2023. SyReNN: a tool for analyzing deep neural networks. International fournal on Software Tools for Technology Transfer 25 2 (2023) 145\u2013165.","DOI":"10.1007\/s10009-023-00695-1"},{"key":"e_1_3_1_73_2","doi-asserted-by":"crossref","unstructured":"Matthew Sotoudeh and Aditya V Thakur. 2020. Abstract neural networks. In Static Analysis: 27th International Symposium SAS 2020 Virtual Event November 18-20 2020 Proceedings 27. Springer 65\u201388.","DOI":"10.1007\/978-3-030-65474-0_4"},{"key":"e_1_3_1_74_2","doi-asserted-by":"crossref","unstructured":"Marcelo Sousa and Isil Dillig. 2016. Cartesian hoare logic for verifying k-safety properties. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation PLDI 2016 Santa Barbara CA USA June 13-17 2016 Chandra Krintz and Emery D. Berger (Eds.). ACM 57\u201369. https:\/\/doi.org\/10.1145\/2908080.2908092","DOI":"10.1145\/2908080.2908092"},{"key":"e_1_3_1_75_2","doi-asserted-by":"crossref","unstructured":"Cheng Tan Yibo Zhu and Chuanxiong Guo. 2021. Building Verified Neural Networks with Specifications for Systems. In Proceedings of the 12th ACM SIGOPS Asia-Pacific Workshop on Systems (Hong Kong China) (APSys \u201821). 42\u201347.","DOI":"10.1145\/3476886.3477508"},{"key":"e_1_3_1_76_2","doi-asserted-by":"crossref","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 Formal Methods - The Next 30 Years Maurice H. ter Beek Annabelle McIver and Jos\u00e9 N. Oliveira (Eds.). Springer International Publishing Cham 670-686","DOI":"10.1007\/978-3-030-30942-8_39"},{"key":"e_1_3_1_77_2","doi-asserted-by":"publisher","DOI":"10.1145\/3527319"},{"key":"e_1_3_1_78_2","doi-asserted-by":"crossref","unstructured":"Hiroshi Unno Tachio Terauchi and Eric Koskinen. 2021. Constraint-Based Relational Verification. In Computer Aided Verification - 33rd International Conference CAV 2021 Virtual Event July 20-23 2021 Proceedings Part I (Lecture Proc. ACM Program. Lang. Vol. 8 No. PLDI Article 147. Publication date: June 2024. Notes in Computer Science Vol. 12759) Alexandra Silva and K. Rustan M. Leino (Eds.). Springer 742\u2013766. https:\/\/doi.org\/10.1007\/978-3-030-81685-8_35","DOI":"10.1007\/978-3-030-81685-8_35"},{"key":"e_1_3_1_79_2","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."},{"key":"e_1_3_1_80_2","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 (2021)."},{"key":"e_1_3_1_81_2","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 Neural Network Robustness Verification. In Advances in Neural Information Processing Systems A. Beygelzimer Y. Dauphin P. Liang and J. Wortman Vaughan (Eds.). https:\/\/openreview.net\/forum?id=ahYIIRBeCFw"},{"key":"e_1_3_1_82_2","doi-asserted-by":"crossref","unstructured":"Zhilu Wang Chao Huang and Qi Zhu. 2022. Efficient global robustness certification of neural networks via interleaving twin-network encoding. In 2022 Design Automation & Test in Europe Conference & Exhibition (DATE). IEEE 1087\u20131092.","DOI":"10.23919\/DATE54114.2022.9774719"},{"key":"e_1_3_1_83_2","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 2018 Stockholmsm\u00e4ssan Stockholm Sweden July 10-15 2018 (Proceedings of Machine Learning Research Vol. 80) Jennifer G. Dy and Andreas Krause (Eds.). PMLR 5283\u20135292. http:\/\/proceedings.mlr.press\/v80\/wong18a.html"},{"key":"e_1_3_1_84_2","author":"Wu Haoze","year":"2022","unstructured":"Haoze Wu, Clark Barrett, Mahmood Sharif, Nina Narodytska, and Gagandeep Singh. 2022. Scalable Verification of GNN-Based Job Schedulers. Proc. ACM Program. Lang. 6, OOPSLA2, Article 162 (oct 2022), 30 pages. https:\/\/doi.org \/10.1145\/3563325","journal-title":"Proc. ACM Program"},{"key":"e_1_3_1_85_2","doi-asserted-by":"crossref","unstructured":"Haoze Wu Teruhiro Tagomori Alexander Robey Fengjun Yang Nikolai Matni George Pappas Hamed Hassani Corina Pasareanu and Clark Barrett. 2023. Toward certified robustness against real-world distribution shifts. In 2023 IEEE Conference on Secure and Trustworthy Machine Learning (SaTML). IEEE 537\u2013553.","DOI":"10.1109\/SaTML54575.2023.00042"},{"key":"e_1_3_1_86_2","unstructured":"Changming Xu and Gagandeep Singh. 2022. Robust Universal Adversarial Perturbations. CoRR abs\/2206.10858 (2022). https:\/\/doi.org\/10.48550\/arXiv.2206.10858 arXiv:2206.10858"},{"key":"e_1_3_1_87_2","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. (2020)."},{"key":"e_1_3_1_88_2","unstructured":"Kaidi Xu Huan Zhang Shiqi Wang Yihan Wang Suman Jana Xue Lin and Cho-Jui Hsieh. 2021. Fast and Complete Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers. In International Conference on Learning Representations. https:\/\/openreview.net\/forum?id=nVZtXBI6LNn"},{"key":"e_1_3_1_89_2","unstructured":"Yi Zeng Zhouxing Shi Ming Jin Feiyang Kang Lingjuan Lyu Cho-Jui Hsieh and Ruoxi Jia. 2023. Towards Robustness Certification Against Universal Perturbations. In The Eleventh International Conference on Learning Representations. https:\/\/openreview.net\/forum?id=7GEvPKxjtt"},{"key":"e_1_3_1_90_2","unstructured":"Mustafa Zeqiri Mark Niklas M\u00fcller Marc Fischer and Martin T. Vechev. 2023. Efficient Certified Training and Robustness Verification of Neural ODEs. In The Eleventh International Conference on Learning Representations ICLR 2023 Kigali Rwanda May 1\u20135 2023. OpenReview.net. https:\/\/openreview.net\/pdf?id=KyoVpYvWWnK"},{"key":"e_1_3_1_91_2","article-title":"Towards stable and efficient training of verifiably robust neural networks","author":"Zhang Huan","year":"2020","unstructured":"Huan Zhang, Hongge Chen, Chaowei Xiao, Sven Gowal, Robert Stanforth, Bo Li, Duane Boning, and Cho-Jui Hsieh. 2020. Towards stable and efficient training of verifiably robust neural networks. In Proc. International Conference on Learning Representations (ICLR).","journal-title":"Proc. International Conference on Learning Representations (ICLR)"},{"key":"e_1_3_1_92_2","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"},{"key":"e_1_3_1_93_2","volume-title":"Advances in neural information processing systems","author":"Zhang Huan","year":"2018","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. Advances in neural information processing systems 31 (2018)."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656377","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3656377","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:42:22Z","timestamp":1751661742000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656377"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,20]]},"references-count":92,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2024,6,20]]}},"alternative-id":["10.1145\/3656377"],"URL":"https:\/\/doi.org\/10.1145\/3656377","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,6,20]]},"assertion":[{"value":"2024-06-20","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}