{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T05:42:36Z","timestamp":1761543756118,"version":"build-2065373602"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031999901"},{"type":"electronic","value":"9783031999918"}],"license":[{"start":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:00:00Z","timestamp":1761609600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:00:00Z","timestamp":1761609600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-031-99991-8_3","type":"book-chapter","created":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T05:36:12Z","timestamp":1761543372000},"page":"49-63","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["GRENA: GPU-Aided Abstract Refinement for\u00a0Neural Network Verification"],"prefix":"10.1007","author":[{"given":"Yuyi","family":"Zhong","sequence":"first","affiliation":[]},{"given":"Shaun Zong Zhi","family":"Tan","sequence":"additional","affiliation":[]},{"given":"Hanping","family":"Xu","sequence":"additional","affiliation":[]},{"given":"Siau-Cheng","family":"Khoo","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,10,28]]},"reference":[{"key":"3_CR1","unstructured":"3rd International Verification of Neural Networks Competition (VNN-COMP\u201922) (2022). https:\/\/sites.google.com\/view\/vnn2022"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"Deng, L.: The MNIST database of handwritten digit images for machine learning research [best of the web]. IEEE Signal Process. Mag. 29(6), 141\u2013142 (2012)","DOI":"10.1109\/MSP.2012.2211477"},{"key":"3_CR3","unstructured":"Alpha-beta-crown: A fast and scalable neural network verifier using the bound propagation framework (2025). https:\/\/github.com\/Verified-Intelligence\/alpha-beta-CROWN. Accessed 4 Jan 2025"},{"key":"3_CR4","unstructured":"ETH: ETH Robustness Analyzer for Neural Networks (ERAN) (2025). https:\/\/github.com\/eth-sri\/eran. Accessed 2 Jan 2025"},{"key":"3_CR5","unstructured":"Ferrari, C., M\u00fcller, M.N., Jovanovic, N., Vechev, M.T.: Complete verification via multi-neuron relaxation guided branch-and-bound. In: The Tenth International Conference on Learning Representations, ICLR 2022, Virtual Event, 25\u201329 April 2022. OpenReview.net (2022). https:\/\/openreview.net\/forum?id=l_amHf1oaK"},{"key":"3_CR6","doi-asserted-by":"publisher","unstructured":"Gehr, T., Mirman, M., Drachsler-Cohen, D., Tsankov, P., Chaudhuri, S., Vechev, M.T.: AI2: safety and robustness certification of neural networks with abstract interpretation. In: 2018 IEEE Symposium on Security and Privacy, SP 2018, Proceedings, 21\u201323 May 2018, San Francisco, California, USA, pp. 3\u201318. IEEE Computer Society (2018). https:\/\/doi.org\/10.1109\/SP.2018.00058","DOI":"10.1109\/SP.2018.00058"},{"key":"3_CR7","doi-asserted-by":"publisher","unstructured":"Gowal, S., et al.: Scalable verified training for provably robust image classification. In: 2019 IEEE\/CVF International Conference on Computer Vision, ICCV 2019, Seoul, Korea (South), 27 October\u20132 November 2019, pp. 4841\u20134850. IEEE (2019). https:\/\/doi.org\/10.1109\/ICCV.2019.00494","DOI":"10.1109\/ICCV.2019.00494"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Katz, G., Barrett, C.W., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: an efficient SMT solver for verifying deep neural networks. CoRR abs\/1702.01135 (2017). http:\/\/arxiv.org\/abs\/1702.01135","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"3_CR9","unstructured":"Kotha, S., Brix, C., Kolter, J.Z., Dvijotham, K., Zhang, H.: Provably bounding neural network preimages. In: Oh, A., Naumann, T., Globerson, A., Saenko, K., Hardt, M., Levine, S. (eds.) Advances in Neural Information Processing Systems 36: Annual Conference on Neural Information Processing Systems 2023, NeurIPS 2023, New Orleans, LA, USA, 10\u201316 December 2023 (2023). http:\/\/papers.nips.cc\/paper_files\/paper\/2023\/hash\/fe061ec0ae03c5cf5b5323a2b9121bfd-Abstract-Conference.html"},{"key":"3_CR10","unstructured":"Krizhevsky, A., Nair, V., Hinton, G.: CIFAR-10\/100 (Canadian institute for advanced research). http:\/\/www.cs.toronto.edu\/~kriz\/cifar.html"},{"key":"3_CR11","unstructured":"Gurobi Optimizer (2025). https:\/\/www.gurobi.com\/. Accessed 1 Jan 2025"},{"key":"3_CR12","doi-asserted-by":"publisher","unstructured":"Ma, Z., Li, J., Bai, G.: Relu hull approximation. Proc. ACM Program. Lang. 8(POPL), 2260\u20132287 (2024). https:\/\/doi.org\/10.1145\/3632917","DOI":"10.1145\/3632917"},{"key":"3_CR13","unstructured":"Madry, A., Makelov, A., Schmidt, L., Tsipras, D., Vladu, A.: Towards deep learning models resistant to adversarial attacks. In: 6th International Conference on Learning Representations, ICLR 2018, Vancouver, BC, Canada, 30 April\u20133 May 2018, Conference Track Proceedings. OpenReview.net (2018). https:\/\/openreview.net\/forum?id=rJzIBfZAb"},{"key":"3_CR14","unstructured":"Mirman, M., Gehr, T., Vechev, M.T.: Differentiable abstract interpretation for provably robust neural networks. In: Dy, J.G., Krause, A. (eds.) Proceedings of the 35th International Conference on Machine Learning, ICML 2018, Stockholmsm\u00e4ssan, Stockholm, Sweden, 10\u201315 July 2018. Proceedings of Machine Learning Research, vol.\u00a080, pp. 3575\u20133583. PMLR (2018). http:\/\/proceedings.mlr.press\/v80\/mirman18b.html"},{"key":"3_CR15","unstructured":"M\u00fcller, C., Serre, F., Singh, G., P\u00fcschel, M., Vechev, M.T.: Scaling polyhedral neural network verification on GPUs. In: MLSys. mlsys.org (2021)"},{"key":"3_CR16","unstructured":"M\u00fcller, C., Singh, G., P\u00fcschel, M., Vechev, M.T.: Neural network robustness verification on GPUs. CoRR abs\/2007.10868 (2020). https:\/\/arxiv.org\/abs\/2007.10868"},{"key":"3_CR17","doi-asserted-by":"publisher","unstructured":"M\u00fcller, M.N., Makarchuk, G., Singh, G., P\u00fcschel, M., Vechev, M.T.: PRIMA: general and precise neural network certification via scalable convex hull approximations. Proc. ACM Program. Lang. 6(POPL), 1\u201333 (2022). https:\/\/doi.org\/10.1145\/3498704","DOI":"10.1145\/3498704"},{"key":"3_CR18","doi-asserted-by":"publisher","unstructured":"Paulsen, B., Wang, J., Wang, C.: Reludiff: differential verification of deep neural networks. In: Rothermel, G., Bae, D. (eds.) ICSE 2020: 42nd International Conference on Software Engineering, Seoul, South Korea, 2020, pp. 714\u2013726. ACM (2020). https:\/\/doi.org\/10.1145\/3377811.3380337","DOI":"10.1145\/3377811.3380337"},{"key":"3_CR19","unstructured":"Singh, G., Gehr, T., Mirman, M., P\u00fcschel, M., Vechev, M.T.: Fast and effective robustness certification. In: Bengio, S., Wallach, H.M., Larochelle, H., Grauman, K., Cesa-Bianchi, N., Garnett, R. (eds.) Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, 3\u20138 December 2018, Montr\u00e9al, Canada, pp. 10825\u201310836 (2018). https:\/\/proceedings.neurips.cc\/paper\/2018\/hash\/f2f446980d8e971ef3da97af089481c3-Abstract.html"},{"key":"3_CR20","doi-asserted-by":"publisher","unstructured":"Singh, G., Gehr, T., P\u00fcschel, M., Vechev, M.T.: An abstract domain for certifying neural networks. Proc. ACM Program. Lang. 3(POPL), 41:1\u201341:30 (2019). https:\/\/doi.org\/10.1145\/3290354","DOI":"10.1145\/3290354"},{"key":"3_CR21","unstructured":"Singh, G., Gehr, T., P\u00fcschel, M., Vechev, M.T.: Boosting robustness certification of neural networks. In: 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, 6\u20139 May 2019. OpenReview.net (2019). https:\/\/openreview.net\/forum?id=HJgeEh09KQ"},{"key":"3_CR22","first-page":"21675","volume":"33","author":"C Tjandraatmadja","year":"2020","unstructured":"Tjandraatmadja, C., Anderson, R., Huchette, J., Ma, W., Patel, K.K., Vielma, J.P.: The convex relaxation barrier, revisited: Tightened single-neuron relaxations for neural network verification. Adv. Neural. Inf. Process. Syst. 33, 21675\u201321686 (2020)","journal-title":"Adv. Neural. Inf. Process. Syst."},{"key":"3_CR23","doi-asserted-by":"publisher","unstructured":"Ugare, S., Banerjee, D., Misailovic, S., Singh, G.: Incremental verification of neural networks. Proc. ACM Program. Lang. 7(PLDI), 1920\u20131945 (2023). https:\/\/doi.org\/10.1145\/3591299","DOI":"10.1145\/3591299"},{"key":"3_CR24","doi-asserted-by":"crossref","unstructured":"Ugare, S., Singh, G., Misailovic, S.: Proof transfer for fast certification of multiple approximate neural networks. Proc. ACM Program. Lang. 6(OOPSLA1), 1\u201329 (2022)","DOI":"10.1145\/3527319"},{"key":"3_CR25","doi-asserted-by":"publisher","unstructured":"Urban, C., Christakis, M., W\u00fcstholz, V., Zhang, F.: Perfectly parallel fairness certification of neural networks. Proc. ACM Program. Lang. 4(OOPSLA), 185:1\u2013185:30 (2020). https:\/\/doi.org\/10.1145\/3428253","DOI":"10.1145\/3428253"},{"key":"3_CR26","unstructured":"Wang, S., Pei, K., Whitehouse, J., Yang, J., Jana, S.: Efficient formal safety analysis of neural networks. In: Bengio, S., Wallach, H.M., Larochelle, H., Grauman, K., Cesa-Bianchi, N., Garnett, R. (eds.) Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, 3\u20138 December 2018, Montr\u00e9al, Canada, pp. 6369\u20136379 (2018). https:\/\/proceedings.neurips.cc\/paper\/2018\/hash\/2ecd2bd94734e5dd392d8678bc64cdab-Abstract.html"},{"key":"3_CR27","unstructured":"Wang, S., Pei, K., Whitehouse, J., Yang, J., Jana, S.: Formal security analysis of neural networks using symbolic intervals. In: Enck, W., Felt, A.P. (eds.) 27th USENIX Security Symposium, USENIX Security 2018, Baltimore, MD, USA, 15\u201317 August 2018. USENIX Association (2018). https:\/\/www.usenix.org\/conference\/usenixsecurity18\/presentation\/wang-shiqi"},{"key":"3_CR28","unstructured":"Wang, S., et al.: Beta-crown: efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification. CoRR abs\/2103.06624 (2021). https:\/\/arxiv.org\/abs\/2103.06624"},{"key":"3_CR29","unstructured":"Weng, T., et al.: Towards fast computation of certified robustness for relu networks. In: Dy, J.G., Krause, A. (eds.) Proceedings of the 35th International Conference on Machine Learning, ICML 2018, Stockholmsm\u00e4ssan, Stockholm, Sweden, 10\u201315 July 2018. Proceedings of Machine Learning Research, vol.\u00a080, pp. 5273\u20135282. PMLR (2018). http:\/\/proceedings.mlr.press\/v80\/weng18a.html"},{"key":"3_CR30","unstructured":"Xu, K., et al.: Automatic perturbation analysis for scalable certified robustness and beyond. In: Larochelle, H., Ranzato, M., Hadsell, R., Balcan, M., Lin, H. (eds.) Advances in Neural Information Processing Systems 33: Annual Conference on Neural Information Processing Systems 2020, NeurIPS 2020, 6\u201312 December 2020, virtual (2020). https:\/\/proceedings.neurips.cc\/paper\/2020\/hash\/0cbc5671ae26f67871cb914d81ef8fc1-Abstract.html"},{"key":"3_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/978-3-030-72016-2_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P Yang","year":"2021","unstructured":"Yang, P., et al.: Improving neural network verification through spurious region guided refinement. In: Groote, J.F., Larsen, K.G. (eds.) TACAS 2021. LNCS, vol. 12651, pp. 389\u2013408. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72016-2_21"},{"key":"3_CR32","doi-asserted-by":"publisher","unstructured":"Zelazny, T., Wu, H., Barrett, C.W., Katz, G.: On optimizing back-substitution methods for neural network verification. In: Griggio, A., Rungta, N. (eds.) 22nd Formal Methods in Computer-Aided Design, FMCAD 2022, Trento, Italy, 17\u201321 October 2022, pp. 17\u201326. IEEE (2022). https:\/\/doi.org\/10.34727\/2022\/ISBN.978-3-85448-053-2_7","DOI":"10.34727\/2022\/ISBN.978-3-85448-053-2_7"},{"key":"3_CR33","unstructured":"Zhang, H., Weng, T., Chen, P., Hsieh, C., Daniel, L.: Efficient neural network robustness certification with general activation functions. In: Bengio, S., Wallach, H.M., Larochelle, H., Grauman, K., Cesa-Bianchi, N., Garnett, R. (eds.) Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, 3\u20138 December 2018, Montr\u00e9al, Canada, pp. 4944\u20134953 (2018). https:\/\/proceedings.neurips.cc\/paper\/2018\/hash\/d04863f100d59b3eb688a11f95b0ae60-Abstract.html"},{"key":"3_CR34","doi-asserted-by":"publisher","unstructured":"Zhong, Y., Ta, Q., Khoo, S.: ARENA: enhancing abstract refinement for neural network verification. In: Dragoi, C., Emmi, M., Wang, J. (eds.) Verification, Model Checking, and Abstract Interpretation - 24th International Conference, VMCAI 2023, Boston, MA, USA, 16\u201317 January 2023, Proceedings. Lecture Notes in Computer Science, vol. 13881, pp. 366\u2013388. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-24950-1_17","DOI":"10.1007\/978-3-031-24950-1_17"}],"container-title":["Lecture Notes in Computer Science","AI Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-99991-8_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T05:36:24Z","timestamp":1761543384000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-99991-8_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,28]]},"ISBN":["9783031999901","9783031999918"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-99991-8_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025,10,28]]},"assertion":[{"value":"28 October 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"SAIV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on AI Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Zagreb","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Croatia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"saiv2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.aiverification.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}