{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T17:25:26Z","timestamp":1787592326843,"version":"build-2736575974"},"reference-count":53,"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":[{"DOI":"10.13039\/501100001691","name":"Japan Society for the Promotion of Science","doi-asserted-by":"publisher","award":["JP23H03372"],"award-info":[{"award-number":["JP23H03372"]}],"id":[{"id":"10.13039\/501100001691","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002241","name":"Japan Science and Technology Agency","doi-asserted-by":"publisher","award":["JPMJBY24D7, JPMJMI20B8"],"award-info":[{"award-number":["JPMJBY24D7, JPMJMI20B8"]}],"id":[{"id":"10.13039\/501100002241","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000923","name":"Australian Research Council","doi-asserted-by":"publisher","award":["FT220100391, DP250101396"],"award-info":[{"award-number":["FT220100391, DP250101396"]}],"id":[{"id":"10.13039\/501100000923","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":[[2025,4,9]]},"abstract":"<jats:p>\n                    Incremental verification is an emerging neural network verification approach that aims to accelerate the verification of a neural network\n                    <jats:italic toggle=\"yes\">N*<\/jats:italic>\n                    by reusing the existing verification result (called a\n                    <jats:italic toggle=\"yes\">template<\/jats:italic>\n                    ) of a similar neural network\n                    <jats:italic toggle=\"yes\">N<\/jats:italic>\n                    . To date, the state\u2010of\u2010the\u2010art incremental verification approach leverages the problem splitting history produced by\n                    <jats:italic toggle=\"yes\">branch and bound<\/jats:italic>\n                    (\n                    <jats:monospace>BaB<\/jats:monospace>\n                    ) in verification of\n                    <jats:italic toggle=\"yes\">N<\/jats:italic>\n                    , to select only a part of the sub\u2010problems for verification of\n                    <jats:italic toggle=\"yes\">N*<\/jats:italic>\n                    , thus more efficient than verifying\n                    <jats:italic toggle=\"yes\">N*<\/jats:italic>\n                    from scratch. While this approach identifies whether each sub\u2010problem should be re\u2010assessed, it neglects the information of\n                    <jats:italic toggle=\"yes\">how necessary<\/jats:italic>\n                    each sub\u2010problem should be re\u2010assessed, in the sense that the sub\u2010problems that are more likely to contain counterexamples should be prioritized, in order to terminate the verification process as soon as a counterexample is detected.\n                  <\/jats:p>\n                  <jats:p>\n                    To bridge this gap, we first define a counterexample\n                    <jats:italic toggle=\"yes\">potentiality order<\/jats:italic>\n                    over different sub\u2010problems based on the template, and then we propose Olive, an incremental verification approach that explores the sub\u2010problems of verifying\n                    <jats:italic toggle=\"yes\">N*<\/jats:italic>\n                    orderly guided by counterexample potentiality. Specifically, Olive has two variants, including Olive\n                    <jats:sup>g<\/jats:sup>\n                    , a greedy strategy that always prefers to exploit the sub\u2010problems that are more likely to contain counterexamples, and Olive\n                    <jats:sup>b<\/jats:sup>\n                    , a balanced strategy that also explores the sub\u2010problems that are less likely, in case the template is not sufficiently precise. We experimentally evaluate the efficiency of Olive on 1445 verification problem instances derived from 15 neural networks spanning over two datasets\n                    <jats:monospace>MNIST<\/jats:monospace>\n                    and\n                    <jats:monospace>CIFAR\u201010<\/jats:monospace>\n                    . Our evaluation demonstrates significant performance advantages of Olive over state\u2010of\u2010the\u2010art classic verification and incremental approaches. In particular, Olive shows evident superiority on the problem instances that contain counterexamples, and performs as well as Ivan on the certified problem instances.\n                  <\/jats:p>","DOI":"10.1145\/3720417","type":"journal-article","created":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T13:48:26Z","timestamp":1744206506000},"page":"85-112","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Efficient Incremental Verification of Neural Networks Guided by Counterexample Potentiality"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3844-8180","authenticated-orcid":false,"given":"Guanqin","family":"Zhang","sequence":"first","affiliation":[{"name":"UNSW Sydney, Kensington, Australia"},{"name":"CSIRO's Data61, Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3854-9846","authenticated-orcid":false,"given":"Zhenya","family":"Zhang","sequence":"additional","affiliation":[{"name":"Kyushu University, Fukuoka, Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2927-5628","authenticated-orcid":false,"given":"H.M.N. Dilum","family":"Bandara","sequence":"additional","affiliation":[{"name":"CSIRO's Data61, Sydney, Australia"},{"name":"UNSW Sydney, Kensington, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4603-0024","authenticated-orcid":false,"given":"Shiping","family":"Chen","sequence":"additional","affiliation":[{"name":"CSIRO's Data61, Sydney, Australia"},{"name":"UNSW Sydney, Kensington, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8083-4352","authenticated-orcid":false,"given":"Jianjun","family":"Zhao","sequence":"additional","affiliation":[{"name":"Kyushu University, Fukuoka, Japan"}],"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, Kensington, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_3_1_2_2","article-title":"The Fourth International Verification of Neural Networks Competition (VNN-COMP 2023): Summary and Results.","author":"Brix Christopher","year":"2023","unstructured":"Christopher Brix, Stanley Bak, Changliu Liu, and Taylor T Johnson. 2023a. The Fourth International Verification of Neural Networks Competition (VNN-COMP 2023): Summary and Results. arXiv preprint arXiv:2312.16760 (2023).","journal-title":"arXiv preprint arXiv:2312.16760"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-023-00703-4"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCIAIG.2012.2186810"},{"key":"e_1_3_1_5_2","first-page":"1","article-title":"Branch and bound for piecewise linear neural network verification.","volume":"21","author":"Bunel Rudy","year":"2020","unstructured":"Rudy Bunel, Jingyue Lu, Ilker Turkaslan, Philip HS Torr, Pushmeet Kohli, and M Pawan Kumar 2020. Branch and bound for piecewise linear neural network verification. Journal of Machine Learning Research 21 (2020), 1\u201339.","journal-title":"Journal of Machine Learning Research"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-68167-2_18"},{"key":"e_1_3_1_7_2","article-title":"Scaling the convex barrier with active sets.","author":"De Palma Alessandro","year":"2021","unstructured":"Alessandro De Palma, Harkirat S Behl, Rudy Bunel, and Philip HS Torr 2021a. Scaling the convex barrier with active sets. In ICLR 2021 Conf. Open Review.","journal-title":"ICLR 2021 Conf. Open Review"},{"key":"e_1_3_1_8_2","article-title":"Improved branch and bound for neural network verification via lagrangian decomposition.","author":"De Palma Alessandro","year":"2021","unstructured":"Alessandro De Palma, Rudy Bunel, Alban Desmaison, Krishnamurthy Dwivedi, Pushmeet Kohli, Philip HS Torr, and M Pawan Kumar 2021b. Improved branch and bound for neural network verification via lagrangian decomposition. arXiv preprint arXiv:2104.06718 (2021).","journal-title":"arXiv preprint arXiv:2104.06718"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53288-8_3"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-15839-1_14"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-16722-6_10"},{"key":"e_1_3_1_12_2","article-title":"Complete verification via multi-neuron relaxation guided branch-and-bound.","author":"Ferrari Claudio","year":"2022","unstructured":"Claudio Ferrari, Mark Niklas M\u00fcller, Nikola Jovanovic, and Martin Vechev 2022. Complete verification via multi-neuron relaxation guided branch-and-bound. arXiv preprint arXiv:2205.00263 (2022).","journal-title":"arXiv preprint arXiv:2205.00263"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13185-1_8"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10601-018-9285-6"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2018.00058"},{"key":"e_1_3_1_16_2","first-page":"11","article-title":"Explaining and Harnessing Adversarial Examples.","author":"Goodfellow Ian J.","year":"2015","unstructured":"Ian J. Goodfellow, Jonathon Shlens, and Christian Szegedy 2015. Explaining and Harnessing Adversarial Examples. In 3rd Int. Conf. on Learning Representations (ICLR\u201915). Int. Conf. on Learning Representations, ICLR, San Diego, CA, United States, 11 pages.","journal-title":"3rd Int. Conf. on Learning Representations (ICLR\u201915)"},{"key":"e_1_3_1_17_2","unstructured":"Google LLC. [n.d.]. G Suite. https:\/\/gsuite.google.com."},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1109\/ISSRE52982.2021.00044"},{"key":"e_1_3_1_19_2","unstructured":"Gurobi Optimization LLC. 2023. Gurobi Optimizer Reference Manual. https:\/\/www.gurobi.com."},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-4_13"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2206.00512"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_26"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2019.00108"},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","DOI":"10.1142\/S0218213021503660"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v36i7.20689"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.1561\/2400000035"},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632917"},{"key":"e_1_3_1_29_2","first-page":"27","article-title":"Towards Deep Learning Models Resistant to Adversarial Attacks.","author":"Madry Aleksander","year":"2018","unstructured":"Aleksander Madry, Aleksandar Makelov, Ludwig Schmidt, Dimitris Tsipras, and Adrian Vladoiu 2018. Towards Deep Learning Models Resistant to Adversarial Attacks. In 6th Int. Conf. on Learning Representations (ICLR\u201918). Vancouver, Canada, 27 pages.","journal-title":"6th Int. Conf. on Learning Representations (ICLR\u201918)"},{"key":"e_1_3_1_30_2","article-title":"The third international verification of neural networks competition (VNN-COMP 2022): summary and results.","author":"M\u00fcller Mark Niklas","year":"2022","unstructured":"Mark Niklas M\u00fcller, Christopher Brix, Stanley Bak, Changliu Liu, and Taylor T Johnson 2022a. The third international verification of neural networks competition (VNN-COMP 2022): summary and results. arXiv preprint arXiv:2212.10376 (2022).","journal-title":"arXiv preprint arXiv:2212.10376"},{"key":"e_1_3_1_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/3498704"},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/3377811.3380337"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/3324884.3416560"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132785"},{"key":"e_1_3_1_35_2","first-page":"12","article-title":"Fast and Effective Robustness Certification.","author":"Singh Gangdeep","year":"2018","unstructured":"Gangdeep Singh, Timon Gehn, Matthew Mirman, Markus P\u00fcschel, and Martin Vechev 2018. Fast and Effective Robustness Certification. In Advances in Neural Information Processing Systems, Vol. 31, 12 pages.","journal-title":"Advances in Neural Information Processing Systems"},{"key":"e_1_3_1_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290354"},{"issue":"1","key":"e_1_3_1_37_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1561\/2200000068","article-title":"Introduction to multi-armed bandits.","volume":"12","author":"Slivkins Aleksandrs","year":"2019","unstructured":"Aleksandrs Slivkins et al. 2019. Introduction to multi-armed bandits. Foundations and Trends\u00ae in Machine Learning 12, 1 (2019), 1\u2013286.","journal-title":"Foundations and Trends\u00ae in Machine Learning"},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3181024"},{"key":"e_1_3_1_39_2","article-title":"Evaluating Robustness of Neural Networks with Mixed Integer Programming.","author":"Tjeng Vincent","year":"2018","unstructured":"Vincent Tjeng, Kai Y. Xiao, and Russ Tedrake 2018. Evaluating Robustness of Neural Networks with Mixed Integer Programming. In Int. Conf. on Learning Representations.","journal-title":"Int. Conf. on Learning Representations"},{"key":"e_1_3_1_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/3591299"},{"key":"e_1_3_1_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/3573719"},{"key":"e_1_3_1_42_2","article-title":"Efficient formal safety analysis of neural networks.","volume":"31","author":"Wang Shiqi","year":"2018","unstructured":"Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana 2018a. Efficient formal safety analysis of neural networks. Advances in Neural Information Processing Systems 31 (2018).","journal-title":"Advances in Neural Information Processing Systems"},{"key":"e_1_3_1_43_2","first-page":"1599","article-title":"Formal security analysis of neural networks using symbolic intervals.","author":"Wang Shiqi","year":"2018","unstructured":"Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana 2018b. Formal security analysis of neural networks using symbolic intervals. In 27th USENIX Security Symp. (USENIX Security 18), 1599\u20131614.","journal-title":"27th USENIX Security Symp. (USENIX Security 18)"},{"key":"e_1_3_1_44_2","first-page":"29909","article-title":"Beta-crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification.","volume":"34","author":"Wang Shiqi","year":"2021","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. Advances in Neural Information Processing Systems 34 (2021), 29909\u201329921.","journal-title":"Advances in Neural Information Processing Systems"},{"key":"e_1_3_1_45_2","article-title":"Online Verification of Deep Neural Networks under Domain or Weight Shift.","author":"Wei Tianhao","year":"2021","unstructured":"Tianhao Wei and Changliu Liu 2021. Online Verification of Deep Neural Networks under Domain or Weight Shift. arXiv preprint arXiv:2106.12732 (2021).","journal-title":"arXiv preprint arXiv:2106.12732"},{"key":"e_1_3_1_46_2","first-page":"5276","article-title":"Towards fast computation of certified robustness for relu networks.","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 Int. Conf. on Machine Learning. PMLR, 5276\u20135285.","journal-title":"Int. Conf. on Machine Learning"},{"key":"e_1_3_1_47_2","first-page":"5286","article-title":"Provable defenses against adversarial examples via the convex outer adversarial polytope.","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 Int. Conf. on Machine Learning. PMLR, 5286\u20135295.","journal-title":"Int. Conf. on Machine Learning"},{"key":"e_1_3_1_48_2","first-page":"11674","article-title":"Tightening robustness verification of convolutional neural networks with fine-grained linear approximation.","author":"Wu Yiting","year":"2021","unstructured":"Yiting Wu and Min Zhang 2021. Tightening robustness verification of convolutional neural networks with fine-grained linear approximation. In AAAI Conf. on Artificial Intelligence, Vol. 35, 11674\u201311681.","journal-title":"AAAI Conf. on Artificial Intelligence"},{"key":"e_1_3_1_49_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-981-99-7584-6_9"},{"key":"e_1_3_1_50_2","article-title":"Incremental Satisfiability Modulo Theory for Verification of Deep Neural Networks.","author":"Yang Pengfei","year":"2023","unstructured":"Pengfei Yang, Zhiming Chi, Zongxin Liu, Mengyu Zhao, Cheng-Chao Huang, Shaowei Cai, and Lijun Zhang 2023. Incremental Satisfiability Modulo Theory for Verification of Deep Neural Networks. arXiv preprint arXiv:2302.06455 (2023).","journal-title":"arXiv preprint arXiv:2302.06455"},{"key":"e_1_3_1_51_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72016-2_21"},{"key":"e_1_3_1_52_2","doi-asserted-by":"crossref","unstructured":"Guanqin Zhang Zhenya Zhang Dilum Bandara Shiping Chen Jianyun Zhao and Yulei Sui 2025. Supplementary material for the paper \u201cEfficient Incremental Verification of Neural Networks Guided by Counterexample Potentiality\u201d. https:\/\/sites.google.com\/view\/olive-nnv.","DOI":"10.1145\/3720417"},{"key":"e_1_3_1_53_2","article-title":"Efficient neural network robustness certification with general activation functions.","volume":"31","author":"Zhang Huan","year":"2018","unstructured":"Huan Zhang, Tsui-Wei Meng, 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).","journal-title":"Advances in Neural Information Processing Systems"},{"key":"e_1_3_1_54_2","doi-asserted-by":"publisher","DOI":"10.1145\/3551349.3556907"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720417","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3720417","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3720417","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T16:29:06Z","timestamp":1787588946000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720417"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,9]]},"references-count":53,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2025,4,9]]}},"alternative-id":["10.1145\/3720417"],"URL":"https:\/\/doi.org\/10.1145\/3720417","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"}}]}}