{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T21:07:42Z","timestamp":1760044062116,"version":"3.40.3"},"publisher-location":"Cham","reference-count":43,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031131844"},{"type":"electronic","value":"9783031131851"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,8,7]],"date-time":"2022-08-07T00:00:00Z","timestamp":1659830400000},"content-version":"vor","delay-in-days":218,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Existing neural network verifiers compute a proof that each input is handled correctly under a given perturbation by propagating a symbolic abstraction of reachable values at each layer. This process is repeated from scratch independently for each input (e.g., image) and perturbation (e.g., rotation), leading to an expensive overall proof effort when handling an entire dataset. In this work, we introduce a new method for reducing this verification cost without losing precision based on a key insight that abstractions obtained at intermediate layers for different inputs and perturbations can overlap or contain each other. Leveraging our insight, we introduce the general concept of shared certificates, enabling proof effort reuse across multiple inputs to reduce overall verification costs. We perform an extensive experimental evaluation to demonstrate the effectiveness of shared certificates in reducing the verification cost on a range of datasets and attack specifications on image classifiers including the popular patch and geometric perturbations. We release our implementation at <jats:ext-link xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" ext-link-type=\"uri\" xlink:href=\"https:\/\/github.com\/eth-sri\/proof-sharing\">https:\/\/github.com\/eth-sri\/proof-sharing<\/jats:ext-link>.<\/jats:p>","DOI":"10.1007\/978-3-031-13185-1_7","type":"book-chapter","created":{"date-parts":[[2022,8,6]],"date-time":"2022-08-06T19:29:09Z","timestamp":1659814149000},"page":"127-148","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Shared Certificates for\u00a0Neural Network Verification"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4157-1235","authenticated-orcid":false,"given":"Marc","family":"Fischer","sequence":"first","affiliation":[]},{"given":"Christian","family":"Sprecher","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9813-0900","authenticated-orcid":false,"given":"Dimitar Iliev","family":"Dimitrov","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9299-2961","authenticated-orcid":false,"given":"Gagandeep","family":"Singh","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0054-9568","authenticated-orcid":false,"given":"Martin","family":"Vechev","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,8,7]]},"reference":[{"key":"7_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/978-3-030-59152-6_5","volume-title":"Automated Technology for Verification and Analysis","author":"P Ashok","year":"2020","unstructured":"Ashok, P., Hashemi, V., K\u0159et\u00ednsk\u00fd, J., Mohr, S.: DeepAbstract: neural network abstraction for accelerating verification. In: Hung, D.V., Sokolsky, O. (eds.) ATVA 2020. LNCS, vol. 12302, pp. 92\u2013107. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-59152-6_5"},{"key":"7_CR2","unstructured":"Bak, S., Liu, C., Johnson, T.T.: The second international verification of neural networks competition. arXiv preprint abs\/2109.00498 (2021)"},{"key":"7_CR3","unstructured":"Balunovic, M., Baader, M., Singh, G., Gehr, T., Vechev, M.T.: Certifying geometric robustness of neural networks. In: Neural Information Processing Systems (NIPS) (2019)"},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"Beyer, D., L\u00f6we, S., Novikov, E., Stahlbauer, A., Wendler, P.: Precision reuse for efficient regression verification. In: Symposium on the Foundations of Software Engineering (SIGSOFT) (2013)","DOI":"10.1145\/2491411.2491429"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-39176-7_1","volume-title":"Model Checking Software","author":"D Beyer","year":"2013","unstructured":"Beyer, D., Wendler, P.: Reuse of verification results - conditional model checking, precision reuse, and verification witnesses. In: Bartocci, E., Ramakrishnan, C.R. (eds.) SPIN 2013. LNCS, vol. 7976, pp. 1\u201317. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39176-7_1"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"AR Bradley","year":"2011","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70\u201387. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-18275-4_7"},{"key":"7_CR7","unstructured":"Bradley, A.R., Somenzi, F., Hassan, Z., Zhang, Y.: An incremental approach to model checking progress properties. In: International Conference on Formal Methods in Computer-Aided Design (FMCAD) (2011)"},{"key":"7_CR8","unstructured":"Brown, T.B., Man\u00e9, D., Roy, A., Abadi, M., Gilmer, J.: Adversarial patch. arXiv preprint abs\/1712.09665 (2017)"},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"Cheng, C., Yan, R.: Continuous safety verification of neural networks. In: Design, Automation and Test in Europe Conference and Exhibition (2021)","DOI":"10.23919\/DATE51398.2021.9473994"},{"key":"7_CR10","unstructured":"Chiang, P., Ni, R., Abdelkader, A., Zhu, C., Studer, C., Goldstein, T.: Certified defenses for adversarial patches. In: Proceedings of International Conference on Learning Representations (ICLR) (2020)"},{"key":"7_CR11","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of Principles of Programming Languages (POPL) (1977)","DOI":"10.1145\/512950.512973"},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proceedings of Principles of Programming Languages (POPL) (1978)","DOI":"10.1145\/512760.512770"},{"key":"7_CR13","unstructured":"Fischer, M., Baader, M., Vechev, M.T.: Certified defense to image transformations via randomized smoothing. In: Neural Information Processing Systems (NIPS) (2020)"},{"key":"7_CR14","doi-asserted-by":"crossref","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: Symposium on Security and Privacy (S &P) (2018)","DOI":"10.1109\/SP.2018.00058"},{"issue":"3","key":"7_CR15","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1007\/s10703-015-0238-z","volume":"47","author":"E Goubault","year":"2016","unstructured":"Goubault, E., Putot, S.: A zonotopic framework for functional abstractions. Formal Methods Syst. Des. 47(3), 302\u2013360 (2016). https:\/\/doi.org\/10.1007\/s10703-015-0238-z","journal-title":"Formal Methods Syst. Des."},{"key":"7_CR16","unstructured":"Gowal, S., et al.: On the effectiveness of interval bound propagation for training verifiably robust models. arXiv preprint abs\/1810.12715 (2018)"},{"key":"7_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-319-63387-9_5","volume-title":"Computer Aided Verification","author":"G Katz","year":"2017","unstructured":"Katz, G., Barrett, C., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: an efficient SMT solver for verifying deep neural networks. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 97\u2013117. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_5"},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/978-3-030-25540-4_26","volume-title":"Computer Aided Verification","author":"G Katz","year":"2019","unstructured":"Katz, G., et al.: The Marabou framework for verification and analysis of deep neural networks. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 443\u2013452. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_26"},{"key":"7_CR19","doi-asserted-by":"crossref","unstructured":"Kopetzki, A., Sch\u00fcrmann, B., Althoff, M.: Methods for order reduction of zonotopes. In: Conference on Decision and Control (CDC) (2017)","DOI":"10.1109\/CDC.2017.8264508"},{"key":"7_CR20","unstructured":"Krizhevsky, A., Hinton, G., et al.: Learning multiple layers of features from tiny images (2009)"},{"key":"7_CR21","unstructured":"Krizhevsky, A., Sutskever, I., Hinton, G.E.: ImageNet classification with deep convolutional neural networks. In: Neural Information Processing Systems (NIPS) (2012)"},{"key":"7_CR22","unstructured":"LeCun, Y., et al.: Handwritten digit recognition with a back-propagation network. In: Neural Information Processing Systems (NIPS) (1989)"},{"key":"7_CR23","unstructured":"Madry, A., Makelov, A., Schmidt, L., Tsipras, D., Vladu, A.: Towards deep learning models resistant to adversarial attacks. In: Proceedings of International Conference on Learning Representations (ICLR) (2018)"},{"key":"7_CR24","unstructured":"Mirman, M., Gehr, T., Vechev, M.T.: Differentiable abstract interpretation for provably robust neural networks. In: Proceedings of International Conference on Machine Learning (ICML), vol. 80 (2018)"},{"key":"7_CR25","unstructured":"Paszke, A., et al.: Pytorch: an imperative style, high-performance deep learning library. In: Neural Information Processing Systems (NIPS) (2019)"},{"key":"7_CR26","doi-asserted-by":"crossref","unstructured":"Paulsen, B., Wang, J., Wang, C.: RELUDIFF: differential verification of deep neural networks. In: International Conference on Software Engineering (ICSE) (2020)","DOI":"10.1145\/3377811.3380337"},{"key":"7_CR27","doi-asserted-by":"crossref","unstructured":"Paulsen, B., Wang, J., Wang, J., Wang, C.: NEURODIFF: scalable differential verification of neural networks using fine-grained approximation. In: Conference on Automated Software Engineering (ASE) (2020)","DOI":"10.1145\/3324884.3416560"},{"key":"7_CR28","unstructured":"Pei, K., Cao, Y., Yang, J., Jana, S.: Towards practical verification of machine learning: the case of computer vision systems. arXiv preprint abs\/1712.01785 (2017)"},{"key":"7_CR29","doi-asserted-by":"crossref","unstructured":"Sadraddini, S., Tedrake, R.: Linear encodings for polytope containment problems. In: Conference on Decision and Control (CDC) (2019)","DOI":"10.1109\/CDC40024.2019.9029363"},{"key":"7_CR30","doi-asserted-by":"crossref","unstructured":"Silver, D., et al.: Mastering the game of go without human knowledge. Nature 550(7676) (2017)","DOI":"10.1038\/nature24270"},{"key":"7_CR31","unstructured":"Singh, G., Gehr, T., Mirman, M., P\u00fcschel, M., Vechev, M.T.: Fast and effective robustness certification. In: Neural Information Processing Systems (NIPS) (2018)"},{"key":"7_CR32","doi-asserted-by":"crossref","unstructured":"Singh, G., Gehr, T., P\u00fcschel, M., Vechev, M.T.: An abstract domain for certifying neural networks. PACMPL 3(POPL) (2019)","DOI":"10.1145\/3290354"},{"key":"7_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/3-540-58179-0_67","volume-title":"Computer Aided Verification","author":"OV Sokolsky","year":"1994","unstructured":"Sokolsky, O.V., Smolka, S.A.: Incremental model checking in the modal mu-calculus. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 351\u2013363. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-58179-0_67"},{"key":"7_CR34","unstructured":"Szegedy, C., et al.: Intriguing properties of neural networks. In: Proceedings of International Conference on Learning Representations (ICLR) (2014)"},{"key":"7_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-030-55754-6_15","volume-title":"NASA Formal Methods","author":"J Taljaard","year":"2020","unstructured":"Taljaard, J., Geldenhuys, J., Visser, W.: Constraint caching revisited. In: Lee, R., Jha, S., Mavridou, A., Giannakopoulou, D. (eds.) NFM 2020. LNCS, vol. 12229, pp. 251\u2013266. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-55754-6_15"},{"key":"7_CR36","doi-asserted-by":"crossref","unstructured":"Visser, W., Geldenhuys, J., Dwyer, M.B.: Green: reducing, reusing and recycling constraints in program analysis. In: Symposium on the Foundations of Software Engineering (SIGSOFT) (2012)","DOI":"10.1145\/2393596.2393665"},{"key":"7_CR37","unstructured":"Wei, T., Liu, C.: Online verification of deep neural networks under domain or weight shift. arXiv preprint abs\/2106.12732 (2021)"},{"key":"7_CR38","unstructured":"Weng, T., et al.: Towards fast computation of certified robustness for ReLu networks. In: Proceedings of International Conference on Machine Learning (ICML), vol. 80 (2018)"},{"key":"7_CR39","doi-asserted-by":"crossref","unstructured":"Wing, J.M.: Trustworthy AI. Commun. ACM 64(10) (2021)","DOI":"10.1145\/3448248"},{"key":"7_CR40","unstructured":"Wong, E., Kolter, J.Z.: Provable defenses against adversarial examples via the convex outer adversarial polytope. In: Proceedings of International Conference on Machine Learning (ICML), vol. 80 (2018)"},{"key":"7_CR41","unstructured":"Yang, G., Dwyer, M.B., Rothermel, G.: Regression model checking. In: International Conference on Software Maintenance (ICSM) (2009)"},{"key":"7_CR42","unstructured":"Zhang, H., Weng, T., Chen, P., Hsieh, C., Daniel, L.: Efficient neural network robustness certification with general activation functions. In: Neural Information Processing Systems (NIPS) (2018)"},{"key":"7_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-89051-3_1","volume-title":"Programming Languages and Systems","author":"Y Zhong","year":"2021","unstructured":"Zhong, Y., Ta, Q.-T., Luo, T., Zhang, F., Khoo, S.-C.: Scalable and modular robustness analysis of deep neural networks. In: Oh, H. (ed.) APLAS 2021. LNCS, vol. 13008, pp. 3\u201322. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-89051-3_1"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-13185-1_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,11,3]],"date-time":"2022-11-03T17:11:59Z","timestamp":1667495519000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-13185-1_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031131844","9783031131851"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-13185-1_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"7 August 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Haifa","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Israel","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 August 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 August 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2022\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"209","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"40","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"19% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.9","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9.7","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}