{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T07:19:23Z","timestamp":1781075963570,"version":"3.54.1"},"publisher-location":"Cham","reference-count":44,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031308222","type":"print"},{"value":"9783031308239","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,4,22]],"date-time":"2023-04-22T00:00:00Z","timestamp":1682121600000},"content-version":"vor","delay-in-days":111,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Occlusion is a prevalent and easily realizable semantic perturbation to deep neural networks (DNNs). It can fool a DNN into misclassifying an input image by occluding some segments, possibly resulting in severe errors. Therefore, DNNs planted in safety-critical systems should be verified to be robust against occlusions prior to deployment. However, most existing robustness verification approaches for DNNs are focused on non-semantic perturbations and are not suited to the occlusion case. In this paper, we propose the first efficient, SMT-based approach for formally verifying the occlusion robustness of DNNs. We formulate the occlusion robustness verification problem and prove it is NP-complete. Then, we devise a novel approach for encoding occlusions as a part of neural networks and introduce two acceleration techniques so that the extended neural networks can be efficiently verified using off-the-shelf, SMT-based neural network verification tools. We implement our approach in a prototype called\n                    <jats:sc>OccRob<\/jats:sc>\n                    and extensively evaluate its performance on benchmark datasets with various occlusion variants. The experimental results demonstrate our approach\u2019s effectiveness and efficiency in verifying DNNs\u2019 robustness against various occlusions, and its ability to generate counterexamples when these DNNs are not robust.\n                  <\/jats:p>","DOI":"10.1007\/978-3-031-30823-9_11","type":"book-chapter","created":{"date-parts":[[2023,4,21]],"date-time":"2023-04-21T16:19:12Z","timestamp":1682093952000},"page":"208-226","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["OccRob: Efficient SMT-Based Occlusion Robustness Verification of Deep Neural Networks"],"prefix":"10.1007","author":[{"given":"Xingwu","family":"Guo","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ziwei","family":"Zhou","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yueling","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Guy","family":"Katz","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1938-2902","authenticated-orcid":false,"given":"Min","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2023,4,22]]},"reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"Amir, G., Wu, H., Barrett, C., Katz, G.: An smt-based approach for verifying binarized neural networks. In: TACAS\u201921. pp. 203\u2013222. Springer (2021)","DOI":"10.1007\/978-3-030-72013-1_11"},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"Boopathy, A., Weng, T.W., Chen, P.Y., Liu, S., Daniel, L.: Cnn-cert: An efficient framework for certifying robustness of convolutional neural networks. In: AAAI\u201919. vol.\u00a033, pp. 3240\u20133247 (2019)","DOI":"10.1609\/aaai.v33i01.33013240"},{"key":"11_CR3","unstructured":"Brown, T.B., Man\u00e9, D., Roy, A., Abadi, M., Gilmer, J.: Adversarial patch. arXiv preprint arXiv:1712.09665 (2017)"},{"key":"11_CR4","unstructured":"Chiang, P.y., Ni, R., Abdelkader, A., Zhu, C., Studer, C., Goldstein, T.: Certified defenses for adversarial patches. arXiv preprint arXiv:2003.06693 (2020)"},{"key":"11_CR5","unstructured":"Cohen, J., Rosenfeld, E., Kolter, Z.: Certified adversarial robustness via randomized smoothing. In: ICML\u201919. pp. 1310\u20131320. PMLR (2019)"},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"Co\u015fkun, M., U\u00e7ar, A., Yildirim, \u00d6., Demir, Y.: Face recognition based on convolutional neural network. In: MEES\u201917. pp. 376\u2013379. IEEE (2017)","DOI":"10.1109\/MEES.2017.8248937"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"Elboher, Y.Y., Gottschlich, J., Katz, G.: An abstraction-based framework for neural network verification. In: CAV\u201920. pp. 43\u201365. Springer (2020)","DOI":"10.1007\/978-3-030-53288-8_3"},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"Eykholt, K., Evtimov, I., Fernandes, E., Li, B., Rahmati, A., Xiao, C., Prakash, A., Kohno, T., Song, D.: Robust physical-world attacks on deep learning visual classification. In: CVPR\u201918. pp. 1625\u20131634 (2018)","DOI":"10.1109\/CVPR.2018.00175"},{"key":"11_CR9","unstructured":"Fischer, M., Baader, M., Vechev, M.: Certified defense to image transformations via randomized smoothing. NeurIPS\u201920 33, 8404\u20138417 (2020)"},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"Gehr, T., Mirman, M., Drachsler-Cohen, D., Tsankov, P., Chaudhuri, S., Vechev, M.: Ai2: Safety and robustness certification of neural networks with abstract interpretation. In: S &P\u201918. pp. 3\u201318. IEEE (2018)","DOI":"10.1109\/SP.2018.00058"},{"key":"11_CR11","unstructured":"Goodfellow, I., Bengio, Y., Courville, A.: Deep Learning, pp. 168\u2013196. MIT Press (2016), http:\/\/www.deeplearningbook.org"},{"key":"11_CR12","unstructured":"Gowal, S., Dvijotham, K., Stanforth, R., Bunel, R., Qin, C., Uesato, J., Arandjelovic, R., Mann, T., Kohli, P.: On the effectiveness of interval bound propagation for training verifiably robust models. arXiv preprint arXiv:1810.12715 (2018)"},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"Gowal, S., Dvijotham, K.D., Stanforth, R., Bunel, R., Qin, C., Uesato, J., Arandjelovic, R., Mann, T., Kohli, P.: Scalable verified training for provably robust image classification. In: ICCV\u201919. pp. 4842\u20134851 (2019)","DOI":"10.1109\/ICCV.2019.00494"},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"Guo, X., Wan, W., Zhang, Z., Zhang, M., Song, F., Wen, X.: Eager falsification for accelerating robustness verification of deep neural networks. In: ISSRE\u201921. pp. 345\u2013356. IEEE (2021)","DOI":"10.1109\/ISSRE52982.2021.00044"},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"Guo, X., Zhou, Z., Zhang, Y., Katz, G., Zhang, M.: OccRob: Efficient smt-based occlusion robustness verification of deep neural networks. arXiv preprint (2023)","DOI":"10.1007\/978-3-031-30823-9_11"},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"Houben, S., Stallkamp, J., Salmen, J., Schlipsing, M., Igel, C.: Detection of traffic signs in real-world images: The German Traffic Sign Detection Benchmark. In: IJCNN\u201913 (2013)","DOI":"10.1109\/IJCNN.2013.6706807"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety verification of deep neural networks. In: CAV\u201917. pp. 3\u201329. Springer (2017)","DOI":"10.1007\/978-3-319-63387-9_1"},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"Islam, M.J., Pan, R., Nguyen, G., Rajan, H.: Repairing deep neural networks: Fix patterns and challenges. In: ICSE\u201920. pp. 1135\u20131146. IEEE (2020)","DOI":"10.1145\/3377811.3380378"},{"key":"11_CR19","unstructured":"Jaderberg, M., Simonyan, K., Zisserman, A., et\u00a0al.: Spatial transformer networks. In: Advances in neural information processing systems. pp. 2017\u20132025. PMLR (2015)"},{"key":"11_CR20","doi-asserted-by":"crossref","unstructured":"Katz, G., Barrett, C., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: An efficient smt solver for verifying deep neural networks. In: CAV\u201917. pp. 97\u2013117. Springer (2017)","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"11_CR21","doi-asserted-by":"crossref","unstructured":"Katz, G., Huang, D.A., Ibeling, D., Julian, K., Lazarus, C., Lim, R., Shah, P., Thakoor, S., Wu, H., Zelji\u0107, A., et\u00a0al.: The Marabou framework for verification and analysis of deep neural networks. In: CAV\u201919. pp. 443\u2013452. Springer (2019)","DOI":"10.1007\/978-3-030-25540-4_26"},{"key":"11_CR22","doi-asserted-by":"crossref","unstructured":"Kirkland, E.J.: Bilinear Interpolation, pp. 261\u2013263. Springer US, Boston, MA (2010)","DOI":"10.1007\/978-1-4419-6533-2_12"},{"key":"11_CR23","doi-asserted-by":"crossref","unstructured":"Kortylewski, A., Liu, Q., Wang, A., Sun, Y., Yuille, A.: Compositional convolutional neural networks: A robust and interpretable model for object recognition under occlusion. International Journal of Computer Vision 129(3), 736\u2013760 (2021)","DOI":"10.1007\/s11263-020-01401-3"},{"key":"11_CR24","unstructured":"LeCun, Y., Cortes, C.: MNIST handwritten digit database (2010), http:\/\/yann.lecun.com\/exdb\/mnist\/"},{"key":"11_CR25","unstructured":"Lengyel, H., Remeli, V., Szalay, Z.: Easily deployed stickers could disrupt traffic sign recognition. Perner\u2019s Contacts 19(Special Issue 2), 156\u2013163 (2019)"},{"key":"11_CR26","doi-asserted-by":"crossref","unstructured":"Li, J., Liu, J., Yang, P., Chen, L., Huang, X., Zhang, L.: Analyzing deep neural networks with symbolic propagation: Towards higher precision and faster verification. In: SAS\u201919. pp. 296\u2013319. Springer (2019)","DOI":"10.1007\/978-3-030-32304-2_15"},{"key":"11_CR27","unstructured":"Lillicrap, T.P., Hunt, J.J., Pritzel, A., Heess, N., Erez, T., Tassa, Y., Silver, D., Wierstra, D.: Continuous control with deep reinforcement learning. arXiv preprint arXiv:1509.02971 (2015)"},{"key":"11_CR28","doi-asserted-by":"crossref","unstructured":"Lyu, Z., Guo, M., Wu, T., Xu, G., Zhang, K., Lin, D.: Towards evaluating and training verifiably robust neural networks. In: CVPR\u201921. pp. 4308\u20134317 (2021)","DOI":"10.1109\/CVPR46437.2021.00429"},{"key":"11_CR29","doi-asserted-by":"crossref","unstructured":"Lyu, Z., Ko, C.Y., Kong, Z., Wong, N., Lin, D., Daniel, L.: Fastened crown: Tightened neural network robustness certificates. In: AAAI\u201920. vol.\u00a034, pp. 5037\u20135044 (2020)","DOI":"10.1609\/aaai.v34i04.5944"},{"key":"11_CR30","doi-asserted-by":"crossref","unstructured":"Mohapatra, J., Weng, T.W., Chen, P.Y., Liu, S., Daniel, L.: Towards verifying robustness of neural networks against a family of semantic perturbations. In: ICCV\u201920. pp. 244\u2013252 (2020)","DOI":"10.1109\/CVPR42600.2020.00032"},{"key":"11_CR31","doi-asserted-by":"crossref","unstructured":"Mziou\u00a0Sallami, M., Ibn\u00a0Khedher, M., Trabelsi, A., Kerboua-Benlarbi, S., Bettebghor, D.: Safety and robustness of deep neural networks object recognition under generic attacks. In: ICONIP\u201919. pp. 274\u2013286. Springer (2019)","DOI":"10.1007\/978-3-030-36808-1_30"},{"key":"11_CR32","doi-asserted-by":"crossref","unstructured":"Nelder, J.A., Mead, R.: A simplex method for function minimization. The computer journal 7(4), 308\u2013313 (1965)","DOI":"10.1093\/comjnl\/7.4.308"},{"key":"11_CR33","doi-asserted-by":"crossref","unstructured":"Pei, K., Cao, Y., Yang, J., Jana, S.: Deepxplore: Automated whitebox testing of deep learning systems. In: SOSP\u201917. pp. 1\u201318 (2017)","DOI":"10.1145\/3132747.3132785"},{"key":"11_CR34","unstructured":"Raghunathan, A., Steinhardt, J., Liang, P.: Certified defenses against adversarial examples. arXiv preprint arXiv:1801.09344 (2018)"},{"key":"11_CR35","doi-asserted-by":"crossref","unstructured":"Singh, G., Gehr, T., P\u00fcschel, M., Vechev, M.: An abstract domain for certifying neural networks. Proceedings of the ACM on Programming Languages 3(POPL), 1\u201330 (2019)","DOI":"10.1145\/3290354"},{"key":"11_CR36","unstructured":"Singh, G., Gehr, T., P\u00fcschel, M., Vechev, M.: Robustness certification with refinement. In: ICLR\u201919 (2019)"},{"key":"11_CR37","doi-asserted-by":"crossref","unstructured":"Song, L., Gong, D., Li, Z., Liu, C., Liu, W.: Occlusion robust face recognition based on mask learning with pairwise differential siamese network. In: ICCV\u201919. pp. 773\u2013782 (2019)","DOI":"10.1109\/ICCV.2019.00086"},{"key":"11_CR38","doi-asserted-by":"crossref","unstructured":"Su, J., Vargas, D.V., Sakurai, K.: One pixel attack for fooling deep neural networks. IEEE Transactions on Evolutionary Computation 23(5), 828\u2013841 (2019)","DOI":"10.1109\/TEVC.2019.2890858"},{"key":"11_CR39","unstructured":"Szegedy, C., Zaremba, W., Sutskever, I., Bruna, J., Erhan, D., Goodfellow, I., Fergus, R.: Intriguing properties of neural networks. arXiv preprint arXiv:1312.6199 (2013)"},{"key":"11_CR40","doi-asserted-by":"crossref","unstructured":"Tian, Y., Pei, K., Jana, S., Ray, B.: Deeptest: Automated testing of deep-neural-network-driven autonomous cars. In: ICSE\u201918. pp. 303\u2013314 (2018)","DOI":"10.1145\/3180155.3180220"},{"key":"11_CR41","doi-asserted-by":"crossref","unstructured":"Usman, M., Gopinath, D., Sun, Y., Noller, Y., P\u0103s\u0103reanu, C.S.: Nn repair: Constraint-based repair of neural network classifiers. In: CAV\u201921. pp. 3\u201325. Springer (2021)","DOI":"10.1007\/978-3-030-81685-8_1"},{"key":"11_CR42","unstructured":"Wang, S., Pei, K., Whitehouse, J., Yang, J., Jana, S.: Efficient formal safety analysis of neural networks. In: NeurIPS\u201918. vol.\u00a031. Curran Associates, Inc. (2018)"},{"key":"11_CR43","unstructured":"Wang, S., Pei, K., Whitehouse, J., Yang, J., Jana, S.: Formal security analysis of neural networks using symbolic intervals. In: USENIX Security\u201918. pp. 1599\u20131614 (2018)"},{"key":"11_CR44","unstructured":"Zhu, H., Tang, P., Park, J., Park, S., Yuille, A.: Robustness of object recognition under extreme occlusion in humans and computational models. arXiv preprint arXiv:1905.04598 (2019)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-30823-9_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T17:07:09Z","timestamp":1781024829000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30823-9_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031308222","9783031308239"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30823-9_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"22 April 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2023\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}