{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T22:50:11Z","timestamp":1768344611049,"version":"3.49.0"},"reference-count":73,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T00:00:00Z","timestamp":1744156800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"NSF","award":["CF-2238079, CCF-2316233, CNS-2148583."],"award-info":[{"award-number":["CF-2238079, CCF-2316233, CNS-2148583."]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,4,9]]},"abstract":"<jats:p>The uninterpretability of Deep Neural Networks (DNNs) hinders their use in safety-critical applications. Abstract Interpretation-based DNN certifiers provide promising avenues for building trust in DNNs. Unsoundness in the mathematical logic of these certifiers can lead to incorrect results. However, current approaches to ensure their soundness rely on manual, expert-driven proofs that are tedious to develop, limiting the speed of developing new certifiers. Automating the verification process is challenging due to the complexity of verifying certifiers for arbitrary DNN architectures and handling diverse abstract analyses.\n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \nWe introduce ProveSound, a novel verification procedure that automates the soundness verification of\n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \nDNN certifiers for arbitrary DNN architectures. Our core contribution is the novel concept of a symbolic DNN, using which, ProveSound reduces the soundness property, a universal quantification over arbitrary DNNs, to a tractable symbolic representation, enabling verification with standard SMT solvers. By formalizing the syntax and operational semantics of ConstraintFlow, a DSL for specifying certifiers, ProveSound efficiently verifies both existing and new certifiers, handling arbitrary DNN architectures.\n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \nOur code is available at https:\/\/github.com\/uiuc-focal-lab\/constraintflow.git<\/jats:p>","DOI":"10.1145\/3720509","type":"journal-article","created":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T13:48:26Z","timestamp":1744206506000},"page":"1802-1830","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Automated Verification of Soundness of DNN Certifiers"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0006-4167-8709","authenticated-orcid":false,"given":"Avaljot","family":"Singh","sequence":"first","affiliation":[{"name":"University of Illinois at Urbana-Champaign, Urbana-Champaign, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-1491-3348","authenticated-orcid":false,"given":"Yasmin Chandini","family":"Sarita","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, Urbana-Champaign, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8140-2321","authenticated-orcid":false,"given":"Charith","family":"Mendis","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, 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, Urbana-Champaign, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"crossref","unstructured":"Aws Albarghouthi. 2021. Introduction to Neural Network Verification. verifieddeeplearning.com. arxiv:2109.10317. http:\/\/verifieddeeplearning.com","DOI":"10.1561\/9781680839111"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.2478\/v10136-012-0031-x"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314614"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3182657"},{"key":"e_1_2_2_5_1","volume-title":"Interpreting Robustness Proofs of Deep Neural Networks. In The Twelfth International Conference on Learning Representations. https:\/\/openreview.net\/forum?id=Ev10F9TWML","author":"Banerjee Debangshu","year":"2024","unstructured":"Debangshu Banerjee, Avaljot Singh, and Gagandeep Singh. 2024. Interpreting Robustness Proofs of Deep Neural Networks. In The Twelfth International Conference on Learning Representations. https:\/\/openreview.net\/forum?id=Ev10F9TWML"},{"key":"e_1_2_2_6_1","volume-title":"Relational DNN Verification With Cross Executional Bound Refinement. In Forty-first International Conference on Machine Learning. https:\/\/openreview.net\/forum?id=HOG80Yk4Gw","author":"Banerjee Debangshu","year":"2024","unstructured":"Debangshu Banerjee and Gagandeep Singh. 2024. Relational DNN Verification With Cross Executional Bound Refinement. In Forty-first International Conference on Machine Learning. https:\/\/openreview.net\/forum?id=HOG80Yk4Gw"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656377"},{"key":"e_1_2_2_8_1","unstructured":"Mariusz Bojarski Davide Testa Daniel Dworakowski Bernhard Firner Beat Flepp Prasoon Goyal Larry Jackel Mathew Monfort Urs Muller Jiakai Zhang Xin Zhang Jake Zhao and Karol Zieba. 2016. End to End Learning for Self-Driving Cars. 04."},{"key":"e_1_2_2_9_1","unstructured":"Akhilan Boopathy Tsui-Wei Weng Pin-Yu Chen Sijia Liu and Luca Daniel. 2019. CNN-Cert: An Efficient Framework for Certifying Robustness of Convolutional Neural Networks. In Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence and Thirty-First Innovative Applications of Artificial Intelligence Conference and Ninth AAAI Symposium on Educational Advances in Artificial Intelligence (AAAI\u201919\/IAAI\u201919\/EAAI\u201919). AAAI Press Article 398 8 pages. isbn:978-1-57735-809-1"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2301.05815"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3238147.3240464"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/800022.808314"},{"key":"e_1_2_2_13_1","volume-title":"Stefano Demarchi and Luca Pulina","author":"Dario Guidotti Armando Tacchella","year":"2023","unstructured":"Armando Tacchella Dario Guidotti, Stefano Demarchi and Luca Pulina. 2023. The Verification of Neural Networks Library (VNN-LIB). https:\/\/www.vnnlib.org, 2023"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_2_15_1","volume-title":"Output Range Analysis for Deep Feedforward Neural Networks","author":"Dutta Souradeep","unstructured":"Souradeep Dutta, Susmit Jha, Sriram Sankaranarayanan, and Ashish Tiwari. 2018. Output Range Analysis for Deep Feedforward Neural Networks. In NASA Formal Methods, Aaron Dutle, C\u00e9sar Mu\u00f1oz, and Anthony Narkawicz (Eds.). Springer International Publishing, Cham. 121\u2013138. isbn:978-3-319-77935-5"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-68167-2_19"},{"key":"e_1_2_2_17_1","volume-title":"International Joint Conference on Automated Reasoning. https:\/\/api.semanticscholar.org\/CorpusID:4508719","author":"Gao Sicun","unstructured":"Sicun Gao, Jeremy Avigad, and Edmund M. Clarke. 2012. \u03b4 -Complete Decision Procedures for Satisfiability over the Reals. In International Joint Conference on Automated Reasoning. https:\/\/api.semanticscholar.org\/CorpusID:4508719"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2018.00058"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/3618408.3618857"},{"key":"e_1_2_2_20_1","volume-title":"Safety Verification of Deep Neural Networks","author":"Huang Xiaowei","unstructured":"Xiaowei Huang, Marta Kwiatkowska, Sen Wang, and Min Wu. 2017. Safety Verification of Deep Neural Networks. In Computer Aided Verification, Rupak Majumdar and Viktor Kun\u010dak (Eds.). Springer International Publishing, Cham. 3\u201329. isbn:978-3-319-63387-9"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2305.06064"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563334"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547628"},{"key":"e_1_2_2_24_1","doi-asserted-by":"crossref","unstructured":"To Van Khanh and Mizuhito Ogawa. 2012. SMT for Polynomial Constraints on Real Numbers. In TAPAS@SAS. https:\/\/api.semanticscholar.org\/CorpusID:13959185","DOI":"10.1016\/j.entcs.2012.11.004"},{"key":"e_1_2_2_25_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Khurshid Sarfraz","unstructured":"Sarfraz Khurshid, Corina S. P\u0102s\u0102reanu, and Willem Visser. 2003. Generalized Symbolic Execution for Model Checking and Testing. In Tools and Algorithms for the Construction and Analysis of Systems, Hubert Garavel and John Hatcliff (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 553\u2013568. isbn:978-3-540-36577-8"},{"key":"e_1_2_2_26_1","doi-asserted-by":"crossref","unstructured":"Rustan Leino and Michal Moskal. 2013. Co-Induction Simply: Automatic Co-Inductive Proofs in a Program Verifier. https:\/\/www.microsoft.com\/en-us\/research\/publication\/co-induction-simply-automatic-co-inductive-proofs-in-a-program-verifier\/","DOI":"10.1007\/978-3-319-06410-9_27"},{"key":"e_1_2_2_27_1","volume-title":"SoK: Certified Robustness for Deep Neural Networks. In 44th IEEE Symposium on Security and Privacy, SP 2023","author":"Li Linyi","year":"2023","unstructured":"Linyi Li, Tao Xie, and Bo Li. 2023. SoK: Certified Robustness for Deep Neural Networks. In 44th IEEE Symposium on Security and Privacy, SP 2023, San Francisco, CA, USA, 22-26 May 2023. IEEE."},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2450136.2450139"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCV48922.2021.00751"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v34i04.5944"},{"key":"e_1_2_2_31_1","volume-title":"International Conference on Learning Representations. https:\/\/openreview.net\/forum?id=rJzIBfZAb","author":"Madry Aleksander","year":"2018","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_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-88806-0_15"},{"key":"e_1_2_2_33_1","volume-title":"Proceedings of the 35th International Conference on Machine Learning, Jennifer Dy and Andreas Krause (Eds.) (Proceedings of Machine Learning Research","volume":"3586","author":"Mirman Matthew","year":"2018","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, Jennifer Dy and Andreas Krause (Eds.) (Proceedings of Machine Learning Research, Vol. 80). PMLR, 3578\u20133586. https:\/\/proceedings.mlr.press\/v80\/mirman18b.html"},{"key":"e_1_2_2_34_1","volume-title":"Proceedings of Machine Learning and Systems 2021","author":"M\u00fcller Christoph","year":"2021","unstructured":"Christoph M\u00fcller, Fran\u00e7ois Serre, Gagandeep Singh, Markus P\u00fcschel, and Martin T. Vechev. 2021. Scaling Polyhedral Neural Network Verification on GPUs. In Proceedings of Machine Learning and Systems 2021, MLSys 2021, virtual, April 5-9, 2021, Alex Smola, Alex Dimakis, and Ion Stoica (Eds.). mlsys.org. https:\/\/proceedings.mlsys.org\/paper\/2021\/hash\/ca46c1b9512a7a8315fa3c5a946e8265-Abstract.html"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498704"},{"key":"e_1_2_2_36_1","volume-title":"SOCRATES: Towards a Unified Platform for Neural Network Verification. ArXiv, abs\/2007.11206","author":"Pham Long H.","year":"2020","unstructured":"Long H. Pham, Jiaying Li, and Jun Sun. 2020. SOCRATES: Towards a Unified Platform for Neural Network Verification. ArXiv, abs\/2007.11206 (2020)."},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/3327546.3327746"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_1"},{"key":"e_1_2_2_39_1","volume-title":"A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks","author":"Salman Hadi","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. Curran Associates Inc., Red Hook, NY, USA."},{"key":"e_1_2_2_40_1","volume-title":"Dwyer","author":"Shriver David","year":"2021","unstructured":"David Shriver, Sebastian Elbaum, and Matthew B. Dwyer. 2021. DNNV: A Framework for Deep Neural Network Verification. In Computer Aided Verification, Alexandra Silva and K. Rustan M. Leino (Eds.). Springer International Publishing, Cham. 137\u2013150. isbn:978-3-030-81685-8"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","unstructured":"A. Singh. 2025. ProveSound: OOPSLA-2025-AEC-final. https:\/\/doi.org\/10.5281\/zenodo.14597703 10.5281\/zenodo.14597703","DOI":"10.5281\/zenodo.14597703"},{"key":"e_1_2_2_42_1","volume-title":"Static Analysis","author":"Singh Avaljot","unstructured":"Avaljot Singh, Yasmin Sarita, Charith Mendis, and Gagandeep Singh. 2024. ConstraintFlow: A DSL for Specification and Verification of Neural Network Analyses. In Static Analysis. Springer Nature Switzerland."},{"key":"e_1_2_2_43_1","volume-title":"Beyond the Single Neuron Convex Barrier for Neural Network Certification","author":"Singh Gagandeep","unstructured":"Gagandeep Singh, Rupanshu Ganvir, Markus P\u00fcschel, and Martin Vechev. 2019. Beyond the Single Neuron Convex Barrier for Neural Network Certification. Curran Associates Inc., Red Hook, NY, USA."},{"key":"e_1_2_2_44_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)."},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290354"},{"key":"e_1_2_2_46_1","volume-title":"Boosting Robustness Certification of Neural Networks. In International Conference on Learning Representations.","author":"Singh Gagandeep","unstructured":"Gagandeep Singh, Timon Gehr, Markus P\u00fcschel, and Martin T. Vechev. 2018. Boosting Robustness Certification of Neural Networks. In International Conference on Learning Representations."},{"key":"e_1_2_2_47_1","volume-title":"Vechev","author":"Singh Gagandeep","year":"2018","unstructured":"Gagandeep Singh, Timon Gehr, Markus P\u00fcschel, and Martin T. Vechev. 2018. ETH Robustness Analyzer for Neural Networks (ERAN). https:\/\/github.com\/eth-sri\/eran"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009885"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-023-00695-1"},{"key":"e_1_2_2_50_1","doi-asserted-by":"crossref","unstructured":"Aditya V. Thakur Akash Lal Junghee Lim and T. Reps. 2015. PostHat and All That: Automating Abstract Interpretation. In TAPAS@SAS. https:\/\/api.semanticscholar.org\/CorpusID:8700802","DOI":"10.1016\/j.entcs.2015.02.003"},{"key":"e_1_2_2_51_1","first-page":"9781713829546","volume-title":"Proceedings of the 34th International Conference on Neural Information Processing Systems (NIPS\u201920)","author":"Tjandraatmadja Christian","year":"2020","unstructured":"Christian Tjandraatmadja, Ross Anderson, Joey Huchette, Will Ma, Krunal Patel, and Juan Pablo Vielma. 2020. The Convex Relaxation Barrier, Revisited: Tightened Single-Neuron Relaxations for Neural Network Verification. In Proceedings of the 34th International Conference on Neural Information Processing Systems (NIPS\u201920). Curran Associates Inc., Red Hook, NY, USA. Article 1819, 12 pages. isbn:9781713829546"},{"key":"e_1_2_2_52_1","volume-title":"Evaluating Robustness of Neural Networks with Mixed Integer Programming. In 7th International Conference on Learning Representations, ICLR 2019","author":"Tjeng Vincent","year":"2019","unstructured":"Vincent Tjeng, Kai Yuanqing Xiao, and Russ Tedrake. 2019. Evaluating Robustness of Neural Networks with Mixed Integer Programming. In 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. OpenReview.net. https:\/\/openreview.net\/forum?id=HyGIdiRqtm"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509578.2509586"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53288-8_2"},{"key":"e_1_2_2_55_1","volume-title":"Patrick Musau, Xiaodong Yang, Luan Viet Nguyen, Weiming Xiang, and Taylor T. Johnson.","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 Formal Methods \u2013 The Next 30 Years, Maurice H. ter Beek, Annabelle McIver, and Jos\u00e9 N. Oliveira (Eds.). Springer International Publishing, Cham. 670\u2013686. isbn:978-3-030-30942-8"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591299"},{"key":"e_1_2_2_57_1","volume-title":"Incremental Randomized Smoothing Certification. In The Twelfth International Conference on Learning Representations. https:\/\/openreview.net\/forum?id=SdeAPV1irk","author":"Ugare Shubham","year":"2024","unstructured":"Shubham Ugare, Tarun Suresh, Debangshu Banerjee, Gagandeep Singh, and Sasa Misailovic. 2024. Incremental Randomized Smoothing Certification. In The Twelfth International Conference on Learning Representations. https:\/\/openreview.net\/forum?id=SdeAPV1irk"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428253"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/1007512.1007526"},{"key":"e_1_2_2_60_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."},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.5555\/3277203.3277323"},{"key":"e_1_2_2_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."},{"key":"e_1_2_2_63_1","volume-title":"Proceedings of the 35th International Conference on Machine Learning, Jennifer Dy and Andreas Krause (Eds.) (Proceedings of Machine Learning Research","volume":"5285","author":"Weng Lily","year":"2018","unstructured":"Lily Weng, Huan Zhang, Hongge Chen, Zhao Song, Cho-Jui Hsieh, Luca Daniel, Duane Boning, and Inderjit Dhillon. 2018. Towards Fast Computation of Certified Robustness for ReLU Networks. In Proceedings of the 35th International Conference on Machine Learning, Jennifer Dy and Andreas Krause (Eds.) (Proceedings of Machine Learning Research, Vol. 80). PMLR, 5276\u20135285. https:\/\/proceedings.mlr.press\/v80\/weng18a.html"},{"key":"e_1_2_2_64_1","volume-title":"Proceedings of the 35th International Conference on Machine Learning, ICML 2018, Stockholmsm\u00e4ssan","author":"Wong Eric","year":"2018","unstructured":"Eric Wong and J. Zico Kolter. 2018. Provable Defenses against Adversarial Examples via the Convex Outer Adversarial Polytope. In Proceedings of the 35th International Conference on Machine Learning, ICML 2018, Stockholmsm\u00e4ssan, Stockholm, Sweden, July 10-15, 2018, Jennifer G. Dy and Andreas Krause (Eds.) (Proceedings of Machine Learning Research, Vol. 80). PMLR, 5283\u20135292. http:\/\/proceedings.mlr.press\/v80\/wong18a.html"},{"key":"e_1_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563325"},{"key":"e_1_2_2_66_1","doi-asserted-by":"publisher","unstructured":"Haoze Wu Alex Ozdemir Aleksandar Zelji\u0107 Kyle Julian Ahmed Irfan Divya Gopinath Sadjad Fouladi Guy Katz Corina Pasareanu and Clark Barrett. 2020. Parallelization Techniques for Verifying Neural Networks. In 2020 Formal Methods in Computer Aided Design (FMCAD). 128\u2013137. https:\/\/doi.org\/10.34727\/2020\/isbn.978-3-85448-042-6_20 10.34727\/2020\/isbn.978-3-85448-042-6_20","DOI":"10.34727\/2020\/isbn.978-3-85448-042-6_20"},{"key":"e_1_2_2_67_1","volume-title":"Johnson","author":"Xiang Weiming","year":"2017","unstructured":"Weiming Xiang, Hoang-Dung Tran, and Taylor T. Johnson. 2017. Output Reachable Set Estimation and Verification for Multi-Layer Neural Networks. CoRR, abs\/1708.03322 (2017), arXiv:1708.03322. arxiv:1708.03322"},{"key":"e_1_2_2_68_1","unstructured":"Changming Xu and Gagandeep Singh. 2023. Robust Universal Adversarial Perturbations. https:\/\/openreview.net\/forum?id=VpYBxaPLaj-"},{"key":"e_1_2_2_69_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."},{"key":"e_1_2_2_70_1","volume-title":"Xue Lin, and Cho-Jui Hsieh.","author":"Xu Kaidi","year":"2020","unstructured":"Kaidi Xu, Huan Zhang, Shiqi Wang, Yihan Wang, Suman Sekhar Jana, Xue Lin, and Cho-Jui Hsieh. 2020. Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers. ArXiv, abs\/2011.13824 (2020)."},{"key":"e_1_2_2_71_1","doi-asserted-by":"publisher","unstructured":"Pengfei Yang Renjue Li Jianlin Li Cheng-Chao Huang Jingyi Wang Jun Sun Bai Xue and Lijun Zhang. 2021. Improving Neural Network Verification through Spurious Region Guided Refinement. 389\u2013408. isbn:978-3-030-72015-5 https:\/\/doi.org\/10.1007\/978-3-030-72016-2_21 10.1007\/978-3-030-72016-2_21","DOI":"10.1007\/978-3-030-72016-2_21"},{"key":"e_1_2_2_72_1","unstructured":"Tom Zelazny Haoze Wu Clark W. Barrett and Guy Katz. 2022. On Optimizing Back-Substitution Methods for Neural Network Verification. 2022 Formal Methods in Computer-Aided Design (FMCAD) 17\u201326."},{"key":"e_1_2_2_73_1","doi-asserted-by":"publisher","DOI":"10.5555\/3327345.3327402"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720509","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3720509","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:15:41Z","timestamp":1760030141000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720509"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,9]]},"references-count":73,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2025,4,9]]}},"alternative-id":["10.1145\/3720509"],"URL":"https:\/\/doi.org\/10.1145\/3720509","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,4,9]]},"assertion":[{"value":"2024-10-16","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-02-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-04-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}