{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,4]],"date-time":"2026-04-04T02:55:31Z","timestamp":1775271331729,"version":"3.50.1"},"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\/"}],"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            <jats:sup>*<\/jats:sup>\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-of-the-art incremental verification approach leverages the problem splitting history produced by\n            <jats:italic toggle=\"yes\">branch and bound (<\/jats:italic>\n            <jats:italic toggle=\"yes\">BaB<\/jats:italic>\n            in verification of\n            <jats:italic toggle=\"yes\">N<\/jats:italic>\n            , to select only a part of the sub-problems for verification of\n            <jats:italic toggle=\"yes\">N<\/jats:italic>\n            <jats:sup>*<\/jats:sup>\n            , thus more efficient than verifying\n            <jats:italic toggle=\"yes\">N<\/jats:italic>\n            <jats:sup>*<\/jats:sup>\n            from scratch. While this approach identifies\n            <jats:italic toggle=\"yes\">whether<\/jats:italic>\n            each sub-problem should be re-assessed, it neglects the information of\n            <jats:italic toggle=\"yes\">how necessary<\/jats:italic>\n            each sub-problem should be re-assessed, in the sense that the sub-problems that are more likely to contain counterexamples should be prioritized, in order to terminate the verification process as soon as a counterexample is detected.                 To bridge this gap, we first define a\n            <jats:italic toggle=\"yes\">counterexample potentiality order<\/jats:italic>\n            over different sub-problems based on the template, and then we propose\n            <jats:italic toggle=\"yes\">Olive<\/jats:italic>\n            , an incremental verification approach that explores the sub-problems of verifying\n            <jats:italic toggle=\"yes\">N<\/jats:italic>\n            <jats:sup>*<\/jats:sup>\n            orderly guided by counterexample potentiality. Specifically,\n            <jats:italic toggle=\"yes\">Olive<\/jats:italic>\n            has two variants, including\n            <jats:italic toggle=\"yes\">Olive<\/jats:italic>\n            <jats:sup>\n              <jats:italic toggle=\"yes\">g<\/jats:italic>\n            <\/jats:sup>\n            , a greedy strategy that always prefers to exploit the sub-problems that are more likely to contain counterexamples, and\n            <jats:italic toggle=\"yes\">Olive<\/jats:italic>\n            <jats:sup>\n              <jats:italic toggle=\"yes\">b<\/jats:italic>\n            <\/jats:sup>\n            , a balanced strategy that also explores the sub-problems that are less likely, in case the template is not sufficiently precise. We experimentally evaluate the efficiency of\n            <jats:italic toggle=\"yes\">Olive<\/jats:italic>\n            on 1445 verification problem instances derived from 15 neural networks spanning over two datasets MNIST and CIFAR-10. Our evaluation demonstrates significant performance advantages of\n            <jats:italic toggle=\"yes\">Olive<\/jats:italic>\n            over state-of-the-art classic verification and incremental approaches. In particular,\n            <jats:italic toggle=\"yes\">Olive<\/jats:italic>\n            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":2,"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":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3854-9846","authenticated-orcid":false,"given":"Zhenya","family":"Zhang","sequence":"additional","affiliation":[{"name":"Kyushu University, Fukuoka, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"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":[{"role":"author","vocabulary":"crossref"}]},{"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":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8083-4352","authenticated-orcid":false,"given":"Jianjun","family":"Zhao","sequence":"additional","affiliation":[{"name":"Kyushu University, Fukuoka, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9510-6574","authenticated-orcid":false,"given":"Yulei","family":"Sui","sequence":"additional","affiliation":[{"name":"UNSW Sydney, Kensington, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_2_1_1_1","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 preprint arXiv:2312.16760."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-023-00703-4"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCIAIG.2012.2186810"},{"key":"e_1_2_1_4_1","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, 42 (2020), 1\u201339.","journal-title":"Journal of Machine Learning Research"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-68167-2_18"},{"key":"e_1_2_1_6_1","volume-title":"ICLR 2021 Conf..","author":"Palma Alessandro De","year":"2021","unstructured":"Alessandro De Palma, Harkirat S Behl, Rudy Bunel, Philip Torr, and M Pawan Kumar. 2021. Scaling the convex barrier with active sets. In ICLR 2021 Conf.."},{"key":"e_1_2_1_7_1","volume-title":"Philip HS Torr, and M Pawan Kumar","author":"Palma Alessandro De","year":"2021","unstructured":"Alessandro De Palma, Rudy Bunel, Alban Desmaison, Krishnamurthy Dvijotham, Pushmeet Kohli, Philip HS Torr, and M Pawan Kumar. 2021. Improved branch and bound for neural network verification via lagrangian decomposition. arXiv preprint arXiv:2104.06718."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53288-8_3"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-15839-1_14"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-16722-6_10"},{"key":"e_1_2_1_11_1","volume-title":"Nikola Jovanovic, and Martin Vechev.","author":"Ferrari Claudio","year":"2022","unstructured":"Claudio Ferrari, Mark Niklas Muller, Nikola Jovanovic, and Martin Vechev. 2022. Complete verification via multi-neuron relaxation guided branch-and-bound. arXiv preprint arXiv:2205.00263."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13185-1_7"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10601-018-9285-6"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2018.00058"},{"key":"e_1_2_1_15_1","volume-title":"Explaining and Harnessing Adversarial Examples. In 3rd Int. Conf. on Learning Representations (ICLR\u201915)","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."},{"key":"e_1_2_1_16_1","unstructured":"Google LLC. [n. d.]. G Suite. https:\/\/gsuite.google.com"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISSRE52982.2021.00044"},{"key":"e_1_2_1_18_1","unstructured":"Gurobi Optimization LLC. 2023. Gurobi Optimizer Reference Manual. https:\/\/www.gurobi.com"},{"key":"e_1_2_1_19_1","volume-title":"DEEPSPLIT: An Efficient Splitting Method for Neural Network Verification via Indirect Effect Analysis.. In IJCAI. 2549\u20132555.","author":"Henriksen Patrick","year":"2021","unstructured":"Patrick Henriksen and Alessio Lomuscio. 2021. DEEPSPLIT: An Efficient Splitting Method for Neural Network Verification via Indirect Effect Analysis.. In IJCAI. 2549\u20132555."},{"key":"e_1_2_1_20_1","volume-title":"Proc. 22nd Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD). 38\u201348","author":"Isac Omri","year":"2022","unstructured":"Omri Isac, Clark Barrett, Min Zhang, and Guy Katz. 2022. Neural network verification with proof production. In Proc. 22nd Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD). 38\u201348."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"e_1_2_1_22_1","doi-asserted-by":"crossref","unstructured":"Guy Katz Derek A Huang Duligur Ibeling Kyle Julian Christopher Lazarus Rachel Lim Parth Shah Shantanu Thakoor Haoze Wu Aleksandar Zelji\u0107 et al. 2019. The marabou framework for verification and analysis of deep neural networks. In Computer Aided Verification Isil Dillig and Serdar Tasiran (Eds.). Springer Int. Publishing 443\u2013452.","DOI":"10.1007\/978-3-030-25540-4_26"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2019.00108"},{"key":"e_1_2_1_24_1","doi-asserted-by":"crossref","unstructured":"Panagiotis Kouvaros and Alessio Lomuscio. 2021. Towards Scalable Complete Verification of Relu Neural Networks via Dependency-based Branching.. In IJCAI. 2643\u20132650.","DOI":"10.24963\/ijcai.2021\/364"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v36i7.20689"},{"key":"e_1_2_1_26_1","doi-asserted-by":"crossref","unstructured":"Changliu Liu Tomer Arnon Christopher Lazarus Christopher Strong Clark Barrett Mykel J Kochenderfer et al. 2021. Algorithms for verifying deep neural networks. Foundations and Trends\u00ae in Optimization 4 3-4 (2021) 244\u2013404.","DOI":"10.1561\/2400000035"},{"key":"e_1_2_1_27_1","volume-title":"POPL","author":"Ma Zhongkui","year":"2024","unstructured":"Zhongkui Ma, Jiaying Li, and Guangdong Bai. 2024. ReLU Hull Approximation. ACM on Programming Languages, 8, POPL (2024), 2260\u20132287."},{"key":"e_1_2_1_28_1","volume-title":"6th Int. Conf. on Learning Representations (ICLR\u201918)","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 6th Int. Conf. on Learning Representations (ICLR\u201918). Vancouver, Canada. 27 pages."},{"key":"e_1_2_1_29_1","unstructured":"Mark Niklas M\u00fcller Christopher Brix Stanley Bak Changliu Liu and Taylor T Johnson. 2022. The third international verification of neural networks competition (VNN-COMP 2022): summary and results. arXiv preprint arXiv:2212.10376."},{"key":"e_1_2_1_30_1","volume-title":"POPL","author":"M\u00fcller Mark Niklas","year":"2022","unstructured":"Mark Niklas M\u00fcller, Gleb Makarchuk, Gagandeep Singh, Markus P\u00fcschel, and Martin Vechev. 2022. PRIMA: general and precise neural network certification via scalable convex hull approximations. ACM on Programming Languages, 6, POPL (2022), 1\u201333."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3377811.3380337"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3324884.3416560"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132785"},{"key":"e_1_2_1_34_1","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. 31 12 pages."},{"key":"e_1_2_1_35_1","volume-title":"POPL","author":"Singh Gagandeep","year":"2019","unstructured":"Gagandeep Singh, Timon Gehr, Markus P\u00fcschel, and Martin Vechev. 2019. An abstract domain for certifying neural networks. ACM on Programming Languages, 3, POPL (2019), 1\u201330."},{"key":"e_1_2_1_36_1","doi-asserted-by":"crossref","unstructured":"Aleksandrs Slivkins et al. 2019. Introduction to multi-armed bandits. Foundations and Trends\u00ae in Machine Learning 12 1-2 (2019) 1\u2013286.","DOI":"10.1561\/2200000068"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180220"},{"key":"e_1_2_1_38_1","volume-title":"Evaluating Robustness of Neural Networks with Mixed Integer Programming. In Int. Conf. on Learning Representations.","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."},{"key":"e_1_2_1_39_1","volume-title":"PLDI (2023)","author":"Ugare Shubham","year":"2023","unstructured":"Shubham Ugare, Debangshu Banerjee, Sasa Misailovic, and Gagandeep Singh. 2023. Incremental Verification of Neural Networks. ACM on Programming Languages, 7, PLDI (2023), 1920\u20131945."},{"key":"e_1_2_1_40_1","volume-title":"OOPSLA1","author":"Ugare Shubham","year":"2022","unstructured":"Shubham Ugare, Gagandeep Singh, and Sasa Misailovic. 2022. Proof transfer for fast certification of multiple approximate neural networks. ACM on Programming Languages, 6, OOPSLA1 (2022), 1\u201329."},{"key":"e_1_2_1_41_1","volume-title":"Efficient formal safety analysis of neural networks. Advances in neural information processing systems, 31","author":"Wang Shiqi","year":"2018","unstructured":"Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. 2018. Efficient formal safety analysis of neural networks. Advances in neural information processing systems, 31 (2018)."},{"key":"e_1_2_1_42_1","volume-title":"27th USENIX Security Symp. (USENIX Security 18)","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 27th USENIX Security Symp. (USENIX Security 18). 1599\u20131614."},{"key":"e_1_2_1_43_1","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_2_1_44_1","unstructured":"Tianhao Wei and Changliu Liu. 2021. Online Verification of Deep Neural Networks under Domain or Weight Shift. arXiv preprint arXiv:2106.12732."},{"key":"e_1_2_1_45_1","volume-title":"Int. Conf. on Machine Learning. 5276\u20135285","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. 5276\u20135285."},{"key":"e_1_2_1_46_1","volume-title":"Int. Conf. on Machine Learning. 5286\u20135295","author":"Wong Eric","year":"2018","unstructured":"Eric Wong and Zico Kolter. 2018. Provable defenses against adversarial examples via the convex outer adversarial polytope. In Int. Conf. on Machine Learning. 5286\u20135295."},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v35i13.17388"},{"key":"e_1_2_1_48_1","volume-title":"Branch and Bound for Sigmoid-Like Neural Network Verification. In Int. Conf. on Formal Engineering Methods. 137\u2013155","author":"Xue Xiaoyong","year":"2023","unstructured":"Xiaoyong Xue and Meng Sun. 2023. Branch and Bound for Sigmoid-Like Neural Network Verification. In Int. Conf. on Formal Engineering Methods. 137\u2013155."},{"key":"e_1_2_1_49_1","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."},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72016-2_21"},{"key":"e_1_2_1_51_1","doi-asserted-by":"crossref","unstructured":"Guanqin Zhang Zhenya Zhang Dilum Bandara Shiping Chen Jianjun 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_2_1_52_1","volume-title":"Efficient neural network robustness certification with general activation functions. Advances in Neural Information Processing Systems, 31","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)."},{"key":"e_1_2_1_53_1","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":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:07:49Z","timestamp":1760029669000},"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"}}]}}