{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,5]],"date-time":"2026-07-05T09:15:55Z","timestamp":1783242955559,"version":"3.54.6"},"publisher-location":"New York, NY, USA","reference-count":24,"publisher":"ACM","license":[{"start":{"date-parts":[[2026,7,5]],"date-time":"2026-07-05T00:00:00Z","timestamp":1783209600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2026,7,5]]},"DOI":"10.1145\/3805760.3814900","type":"proceedings-article","created":{"date-parts":[[2026,7,5]],"date-time":"2026-07-05T08:46:13Z","timestamp":1783241173000},"page":"110-119","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Detecting Unsoundness in Neural Network Verifiers via Concrete\u2013Abstract Consistency"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-2802-0679","authenticated-orcid":false,"given":"Kaijie","family":"Liu","sequence":"first","affiliation":[{"name":"UNSW, Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9510-6574","authenticated-orcid":false,"given":"Yulei","family":"Sui","sequence":"additional","affiliation":[{"name":"UNSW, Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,7,5]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Christopher Brix Stanley Bak Taylor T. Johnson and Haoze Wu. 2024. The Fifth International Verification of Neural Networks Competition (VNN-COMP 2024): Summary and Results. arXiv:2412.19985 [cs.LG]"},{"key":"e_1_3_2_1_2_1","volume-title":"Johnson","author":"Brix Christopher","year":"2023","unstructured":"Christopher Brix, Stanley Bak, Changliu Liu, and Taylor T. Johnson. 2023. The Fourth International Verification of Neural Networks Competition (VNN-COMP 2023): Summary and Results. arXiv:2312.16760 [cs.LG]"},{"key":"e_1_3_2_1_3_1","unstructured":"Alexandra Bugariu. 2022. Automatically Identifying Soundness and Completeness Errors in Program Analysis Tools. Ph. D. Dissertation. ETH Zurich."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_1_5_1","first-page":"47","volume-title":"Proceedings of the 6th Workshop on Formal Methods for ML-Enabled Autonomous Systems","volume":"16","author":"Demarchi Stefano","year":"2023","unstructured":"Stefano Demarchi, Dario Guidotti, Luca Pulina, and Armando Tacchella. 2023. Supporting Standardization of Neural Networks Verification with VNNLIB and CoCoNet. In Proceedings of the 6th Workshop on Formal Methods for ML-Enabled Autonomous Systems, Vol. 16. 47-58."},{"key":"e_1_3_2_1_6_1","volume-title":"2018 IEEE Symposium on Security and Privacy (SP). 3-18","author":"Gehr Timon","year":"2018","unstructured":"Timon Gehr, Matthew Mirman, Dana Drachsler-Cohen, Petar Tsankov, Swarat Chaudhuri, and Martin Vechev. 2018. AI2: Safety and Robustness Certification of Neural Networks with Abstract Interpretation. In 2018 IEEE Symposium on Security and Privacy (SP). 3-18."},{"key":"e_1_3_2_1_7_1","unstructured":"Sven Gowal Krishnamurthy Dvijotham Robert Stanforth Rudy Bunel Chongli Qin Jonathan Uesato Relja Arandjelovic Timothy Mann and Pushmeet Kohli. 2019. On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models. arXiv:1810.12715 [cs.LG]"},{"key":"e_1_3_2_1_8_1","volume-title":"Proc. ACM Softw. Eng. 1, FSE, Article 74 (July","author":"He Weigang","year":"2024","unstructured":"Weigang He, Peng Di, Mengli Ming, Chengyu Zhang, Ting Su, Shijie Li, and Yulei Sui. 2024. Finding and Understanding Defects in Static Analyzers by Constructing Automated Oracles. Proc. ACM Softw. Eng. 1, FSE, Article 74 (July 2024)."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"crossref","first-page":"1466","DOI":"10.1145\/3650212.3680374","volume-title":"Proceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA","author":"Jajal Purvish","year":"2024","unstructured":"Purvish Jajal, Wenxin Jiang, Arav Tewari, Erik Kocinare, Joseph Woo, Anusha Sarraf, Yung-Hsiang Lu, George K. Thiruvathukal, and James C. Davis. 2024. Interoperability in Deep Learning: A User Survey and Failure Analysis of ONNX Model Converters. In Proceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2024). 1466-1478."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3691620.3695034"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1007\/978-3-319-63387-9_5","article-title":"Reluplex","author":"Katz Guy","year":"2017","unstructured":"Guy Katz, Clark Barrett, David L. Dill, Kyle Julian, and Mykel J. Kochenderfer. 2017. Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. In Computer Aided Verification. 97-117.","journal-title":"In Computer Aided Verification."},{"key":"e_1_3_2_1_12_1","first-page":"443","article-title":"The Marabou Framework for Verification and Analysis of Deep Neural Networks","author":"Katz Guy","year":"2019","unstructured":"Guy Katz, Derek A. Huang, Duligur Ibeling, Kyle Julian, Christopher Lazarus, Rachel Lim, Parth Shah, Shantanu Thakoor, Haoze Wu, Aleksandar Zelji\u0107, David L. Dill, Mykel J. Kochenderfer, and Clark Barrett. 2019. The Marabou Framework for Verification and Analysis of Deep Neural Networks. In Computer Aided Verification. 443-452.","journal-title":"Computer Aided Verification."},{"key":"e_1_3_2_1_13_1","volume-title":"6th International Verification of Neural Networks Competition (VNN-COMP 2025)","author":"Kaulen Konstantin","year":"2025","unstructured":"Konstantin Kaulen, Tobias Ladner, Stanley Bak, Christopher Brix, Hai Duong, Thomas Flinkow, Taylor T. Johnson, Lukas Koller, Edoardo Manino, ThanhVu H Nguyen, and Haoze Wu. 2025. The 6th International Verification of Neural Networks Competition (VNN-COMP 2025): Summary and Results. arXiv:2512.19007 [cs.LG]"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293882.3330553"},{"key":"e_1_3_2_1_15_1","volume-title":"An Empirical Study of Challenges in Converting Deep Learning Models. In 2022 IEEE International Conference on Software Maintenance and Evolution (ICSME). 13-23","author":"Openja Moses","year":"2022","unstructured":"Moses Openja, Amin Nikanjam, Ahmed Haj Yahmed, Foutse Khomh, and Zhen Ming Jack Jiang. 2022. An Empirical Study of Challenges in Converting Deep Learning Models. In 2022 IEEE International Conference on Software Maintenance and Evolution (ICSME). 13-23."},{"key":"e_1_3_2_1_16_1","volume-title":"DNNV: A Framework for Deep Neural Network Verification. In Computer Aided Verification: 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part I. 137-150","author":"Shriver David","unstructured":"David Shriver, Sebastian Elbaum, and Matthew B. Dwyer. 2021. DNNV: A Framework for Deep Neural Network Verification. In Computer Aided Verification: 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part I. 137-150."},{"key":"e_1_3_2_1_17_1","volume-title":"Proceedings of the ACM on Programming Languages 9, OOPSLA1 (April 2025)","author":"Singh Avaljot","year":"2025","unstructured":"Avaljot Singh, Yasmin Chandini Sarita, Charith Mendis, and Gagandeep Singh. 2025. Automated Verification of Soundness of DNN Certifiers. Proceedings of the ACM on Programming Languages 9, OOPSLA1 (April 2025), 1802-1830."},{"key":"e_1_3_2_1_18_1","volume-title":"Advances in Neural Information Processing Systems","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. In Advances in Neural Information Processing Systems, Vol. 31."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290354"},{"key":"e_1_3_2_1_20_1","first-page":"58088","volume-title":"Proceedings of the 42nd International Conference on Machine Learning","volume":"267","author":"Sz\u00e1sz Attila","year":"2025","unstructured":"Attila Sz\u00e1sz, Bal\u00e1zs B\u00e1nhelyi, and M\u00e1rk Jelasity. 2025. No Soundness in the Real World: On the Challenges of the Verification of Deployed Neural Networks. In Proceedings of the 42nd International Conference on Machine Learning, Vol. 267. PMLR, 58088-58105."},{"key":"e_1_3_2_1_21_1","volume-title":"Proceedings of the 35th International Conference on Neural Information Processing Systems (NIPS '21)","author":"Wang Shiqi","year":"2021","unstructured":"Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and Zico Kolter. 2021. Beta-CROWN: efficient bound propagation with per-neuron split constraints for neural network robustness verification. In Proceedings of the 35th International Conference on Neural Information Processing Systems (NIPS '21). Article 2289."},{"key":"e_1_3_2_1_22_1","first-page":"5286","volume-title":"Proceedings of the 35th International Conference on Machine Learning","volume":"80","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, Vol. 80. PMLR, 5286-5295."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/3495724.3495820"},{"key":"e_1_3_2_1_24_1","unstructured":"Xingjian Zhou Keyi Shen Andy Xu Hongji Xu Cho-Jui Hsieh Huan Zhang and Zhouxing Shi. 2025. SoundnessBench: A Soundness Benchmark for Neural Network Verifiers. arXiv:2412.03154 [cs.LG]"}],"event":{"name":"AIware '26: 3rd ACM International Conference on AI-Powered Software","location":"Montreal QC Canada","acronym":"AIware '26","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the 3rd ACM International Conference on AI-Powered Software"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3805760.3814900","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,5]],"date-time":"2026-07-05T08:50:21Z","timestamp":1783241421000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3805760.3814900"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,7,5]]},"references-count":24,"alternative-id":["10.1145\/3805760.3814900","10.1145\/3805760"],"URL":"https:\/\/doi.org\/10.1145\/3805760.3814900","relation":{},"subject":[],"published":{"date-parts":[[2026,7,5]]},"assertion":[{"value":"2026-07-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}