{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T17:25:19Z","timestamp":1787592319424,"version":"build-2736575974"},"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\/legalcode"}],"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.<\/jats:p>\n                  <jats:p>\n                    We introduce\n                    <jats:sc>ProveSound<\/jats:sc>\n                    , a novel verification procedure that automates the soundness verification of DNN certifiers for arbitrary DNN architectures. Our core contribution is the novel concept of a\n                    <jats:italic toggle=\"yes\">symbolic DNN,<\/jats:italic>\n                    using which,\n                    <jats:sc>ProveSound<\/jats:sc>\n                    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\n                    <jats:sc>ConstraintFlow<\/jats:sc>\n                    , a DSL for specifying certifiers,\n                    <jats:sc>ProveSound<\/jats:sc>\n                    efficiently verifies both existing and new certifiers, handling arbitrary DNN architectures.\n                  <\/jats:p>\n                  <jats:p>\n                    Our code is available at\n                    <jats:ext-link xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" ext-link-type=\"uri\" xlink:href=\"https:\/\/github.com\/uiuc-focal-lab\/constraintflow.git\">https:\/\/github.com\/uiuc-focal-lab\/constraintflow.git<\/jats:ext-link>\n                  <\/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":4,"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":[{"vocabulary":"crossref","role":"author"}]},{"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":[{"vocabulary":"crossref","role":"author"}]},{"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":[{"vocabulary":"crossref","role":"author"}]},{"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":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"crossref","unstructured":"Aws Albarghouthi. 2021. Introduction to Neural Network Verification. verifieddeeplearning.com. arXiv:2109.10317 [cs.LG] http:\/\/verifieddeeplearning.com.","DOI":"10.1561\/9781680839111"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.2478\/v10136-012-0031-x"},{"key":"e_1_3_2_4_2","doi-asserted-by":"crossref","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.","DOI":"10.1145\/3314221.3314614"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/3182657"},{"key":"e_1_3_2_6_2","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_3_2_7_2","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_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/3656377"},{"key":"e_1_3_2_9_2","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 2016)."},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v33i01.33013240"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","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). CoRR abs\/2301.05815 (2023). doi:10.48550\/arXiv.2301.05815 arXiv:2301.05815","DOI":"10.48550\/arXiv.2301.05815"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/3238147.3240464"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/800022.808314"},{"key":"e_1_3_2_14_2","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_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-77935-5_9"},{"key":"e_1_3_2_17_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_2_18_2","doi-asserted-by":"crossref","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","DOI":"10.1007\/978-3-642-31365-3_23"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","unstructured":"Timon Gehr Matthew Mirman Dana Drachsler-Cohen Petar Tsankov Swarat Chaudhuri and Martin T. Vechev. 2018. AI2: Safety and Robustness Certification of Neural Networks with Abstract Interpretation. In 2018 IEEE Symposium on Security and Privacy SP 2018 Proceedings 21-23 May 2018 San Francisco California USA. 3\u201318. doi:10.1109\/SP.2018.00058","DOI":"10.1109\/SP.2018.00058"},{"key":"e_1_3_2_20_2","unstructured":"Chuqin Geng Nham Le Xiaojie Xu Zhaoyue Wang Arie Gurfinkel and Xujie Si. 2023. Towards Reliable Neural Specifications. In Proceedings of the 40th International Conference on Machine Learning (Honolulu Hawaii USA) (ICML\u201923). JMLR.org Article 449 17 pages."},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_1"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","unstructured":"Omri Isac Yoni Zohar Clark W. Barrett and Guy Katz. 2023. DNN Verification Reachability and the Exponential Function Problem. CoRR abs\/2305.06064 (2023). doi:10.48550\/arXiv.2305.06064 arXiv:2305.06064","DOI":"10.48550\/arXiv.2305.06064"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/3563334"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/3547628"},{"key":"e_1_3_2_25_2","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_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36577-X_40"},{"key":"e_1_3_2_27_2","doi-asserted-by":"crossref","unstructured":"Rustan Leino and Michal Moskal. 2013. Co-Induction Simply: Automatic Co-Inductive Proofs in a Program Verifier. Technical Report MSR-TR-2013-49. 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_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP46215.2023.10179303"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/2450136.2450139"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICCV48922.2021.00751"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v34i04.5944"},{"key":"e_1_3_2_32_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_2_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-88806-0_15"},{"key":"e_1_3_2_34_2","first-page":"3578","volume-title":"Proceedings of the 35th International Conference on Machine Learning (Proceedings of Machine Learning Research, Vol. 80)","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 (Proceedings of Machine Learning Research, Vol. 80), Jennifer Dy and Andreas Krause (Eds.). PMLR, 3578\u20133586. https:\/\/proceedings.mlr.press\/v80\/mirman18b.html"},{"key":"e_1_3_2_35_2","volume-title":"Proceedings of Machine Learning and Systems 2021, MLSys 2021, virtual, April 5-9, 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_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/3498704"},{"key":"e_1_3_2_37_2","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_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.5555\/3327546.3327746"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_1"},{"key":"e_1_3_2_40_2","volume-title":"A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks","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. Curran Associates Inc., Red Hook, NY, USA."},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_6"},{"key":"e_1_3_2_42_2","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_3_2_43_2","volume-title":"Static Analysis","author":"Singh Avaljot","year":"2024","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_3_2_44_2","volume-title":"Beyond the Single Neuron Convex Barrier for Neural Network Certification","author":"Singh Gagandeep","year":"2019","unstructured":"Gagandeep Singh,Rupanshu Ganvir, Markus P\u00fcschel, and Martin Vechev. 2019. Beyond the Single Neuron Convex Barrier for Neural Network Certification. Curran Associates Inc., Red Hook, NY, USA."},{"key":"e_1_3_2_45_2","article-title":"Fast and effective robustness certification","volume":"31","author":"Singh Gagandeep","year":"2018","unstructured":"Gagandeep Singh,Timon Gehr, Matthew Mirman, Markus P\u00fcschel, and Martin Vechev. 2018. Fast and effective robustness certification. Advances in Neural Information Processing Systems 31 (2018).","journal-title":"Advances in Neural Information Processing Systems"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290354"},{"key":"e_1_3_2_47_2","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_3_2_48_2","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_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009885"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-023-00695-1"},{"key":"e_1_3_2_51_2","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_3_2_52_2","first-page":"12","volume-title":"Proceedings of the 34th International Conference on Neural Information Processing Systems (Vancouver, BC, Canada) (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 (Vancouver, BC, Canada) (NIPS\u201920). Curran Associates Inc., Red Hook, NY, USA, Article 1819, 12 pages."},{"key":"e_1_3_2_53_2","volume-title":"7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 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_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.1145\/2509578.2509586"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53288-8_2"},{"key":"e_1_3_2_56_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30942-8_39"},{"key":"e_1_3_2_57_2","doi-asserted-by":"publisher","DOI":"10.1145\/3591299"},{"key":"e_1_3_2_58_2","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_3_2_59_2","doi-asserted-by":"publisher","DOI":"10.1145\/3428253"},{"key":"e_1_3_2_60_2","doi-asserted-by":"publisher","DOI":"10.1145\/1007512.1007526"},{"key":"e_1_3_2_61_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_2_62_2","first-page":"1599","volume-title":"Proceedings of the 27th USENIX Conference on Security Symposium (Baltimore, MD, USA) (SEC\u201918)","author":"Wang Shiqi","year":"2018","unstructured":"Shiqi Wang,Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. 2018. Formal Security Analysis of Neural Networks Using Symbolic Intervals. In Proceedings of the 27th USENIX Conference on Security Symposium (Baltimore, MD, USA) (SEC\u201918). USENIX Association, USA, 1599\u20131614."},{"key":"e_1_3_2_63_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_2_64_2","first-page":"5276","volume-title":"Proceedings of the 35th International Conference on Machine Learning (Proceedings of Machine Learning Research, Vol. 80)","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 (Proceedings of Machine Learning Research, Vol. 80), Jennifer Dy and Andreas Krause (Eds.). PMLR, 5276\u20135285. https:\/\/proceedings.mlr.press\/v80\/weng18a.html"},{"key":"e_1_3_2_65_2","first-page":"5283","volume-title":"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)","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 (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_2_66_2","doi-asserted-by":"publisher","DOI":"10.1145\/3563325"},{"key":"e_1_3_2_67_2","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. doi:10.34727\/2020\/isbn.978-3-85448-042-6_20","DOI":"10.34727\/2020\/isbn.978-3-85448-042-6_20"},{"key":"e_1_3_2_68_2","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 http:\/\/arxiv.org\/abs\/1708.03322"},{"key":"e_1_3_2_69_2","unstructured":"Changming Xu and Gagandeep Singh. 2023. Robust Universal Adversarial Perturbations. https:\/\/openreview.net\/forum?id=VpYBxaPLaj-"},{"key":"e_1_3_2_70_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_2_71_2","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_3_2_72_2","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. doi:10.1007\/978-3-030-72016-2_21","DOI":"10.1007\/978-3-030-72016-2_21"},{"key":"e_1_3_2_73_2","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) (2022) 17\u201326."},{"key":"e_1_3_2_74_2","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":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3720509","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T16:32:42Z","timestamp":1787589162000},"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"}}]}}