{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T09:06:00Z","timestamp":1784797560487,"version":"3.55.0"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032325259","type":"print"},{"value":"9783032325266","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T00:00:00Z","timestamp":1784851200000},"content-version":"vor","delay-in-days":204,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Formal verification of Semantic Segmentation Networks is challenging due to high-dimensional output spaces and cumulative over-approximation errors in deep architectures. Existing verification methods based on specific Star-set reachability suffer from either exponential state explosion (exact splitting) or excessive conservativeness (interval-based relaxation). In this work, we present\n                    <jats:bold>ATKVerifier<\/jats:bold>\n                    , a verification framework for SSNs operating on an abstract domain named constrained-star (C-star), which captures spatial dependencies within MaxPool receptive fields through explicit predicate constraints. Our framework features: (1)\u00a0an adaptive top-K lower bound mechanism that dynamically encodes\n                    <jats:italic>K<\/jats:italic>\n                    potential maximizers based on layer depth and interval overlap, balancing precision and computational cost through parameter-free adaptation; (2) an adaptive affine upper bound exploiting linear relationships between top candidates to replace conservative constant bounds; and (3) region-level completeness (RLC), a spatial robustness metric quantifying the integrity of verified contiguous object regions. Experiments on M2NIST with three SSN architectures (16\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\sim $$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mo>\u223c<\/mml:mo>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    24 layers) demonstrate 8\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\sim $$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mo>\u223c<\/mml:mo>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    25% improvement in robust Intersection-over-Union (IoU) over the ImageStar-based NNV baseline, with the improvement scaling with the network\u2019s depth. For the 24-layer architecture, ATKVerifier achieves 59.2% RLC versus 43.8% of NNV, certifying 35.2% more complete semantic objects.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-32526-6_24","type":"book-chapter","created":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:45:15Z","timestamp":1784796315000},"page":"504-526","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["ATKVerifier: Adaptive Top-K Constraints for\u00a0Tighter Verification of\u00a0Semantic Segmentation Networks"],"prefix":"10.1007","author":[{"given":"Yuehao","family":"Liu","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Cong","family":"Tian","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yansong","family":"Dong","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Liang","family":"Zhao","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Chao","family":"Huang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Wensheng","family":"Wang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,7,24]]},"reference":[{"key":"24_CR1","doi-asserted-by":"publisher","unstructured":"Arnab, A., Miksik, O., Torr, P.H.: On the robustness of semantic segmentation models to adversarial attacks. In: Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition, pp. 888\u2013897 (2018). https:\/\/doi.org\/10.1109\/CVPR.2018.00099","DOI":"10.1109\/CVPR.2018.00099"},{"issue":"12","key":"24_CR2","doi-asserted-by":"publisher","first-page":"2481","DOI":"10.1109\/TPAMI.2016.2644615","volume":"39","author":"V Badrinarayanan","year":"2017","unstructured":"Badrinarayanan, V., Kendall, A., Cipolla, R.: Segnet: a deep convolutional encoder-decoder architecture for image segmentation. IEEE Trans. Pattern Anal. Mach. Intell. 39(12), 2481\u20132495 (2017). https:\/\/doi.org\/10.1109\/TPAMI.2016.2644615","journal-title":"IEEE Trans. Pattern Anal. Mach. Intell."},{"issue":"3","key":"24_CR3","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/s10009-023-00703-4","volume":"25","author":"C Brix","year":"2023","unstructured":"Brix, C., M\u00fcller, M.N., Bak, S., Johnson, T.T., Liu, C.: First three years of the international verification of neural networks competition (VNN-COMP). Int. J. Softw. Tools Technol. Transfer 25(3), 329\u2013339 (2023). https:\/\/doi.org\/10.1007\/s10009-023-00703-4","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"issue":"42","key":"24_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.5555\/3455716.3455758","volume":"21","author":"R Bunel","year":"2020","unstructured":"Bunel, R., Lu, J., Turkaslan, I., Torr, P.H., Kohli, P., Kumar, M.P.: Branch and bound for piecewise linear neural network verification. J. Mach. Learn. Res. 21(42), 1\u201339 (2020). https:\/\/doi.org\/10.5555\/3455716.3455758","journal-title":"J. Mach. Learn. Res."},{"issue":"4","key":"24_CR5","doi-asserted-by":"publisher","first-page":"834","DOI":"10.1109\/TPAMI.2017.2699184","volume":"40","author":"LC Chen","year":"2017","unstructured":"Chen, L.C., Papandreou, G., Kokkinos, I., Murphy, K., Yuille, A.L.: Deeplab: semantic image segmentation with deep convolutional nets, Atrous convolution, and fully connected CRFs. IEEE Trans. Pattern Anal. Mach. Intell. 40(4), 834\u2013848 (2017). https:\/\/doi.org\/10.1109\/TPAMI.2017.2699184","journal-title":"IEEE Trans. Pattern Anal. Mach. Intell."},{"key":"24_CR6","doi-asserted-by":"publisher","unstructured":"Cohen, J., Rosenfeld, E., Kolter, Z.: Certified adversarial robustness via randomized smoothing. In: International Conference on Machine Learning, pp. 1310\u20131320. PMLR (2019). https:\/\/doi.org\/10.48550\/arXiv.1902.02918","DOI":"10.48550\/arXiv.1902.02918"},{"key":"24_CR7","doi-asserted-by":"publisher","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 the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pp. 238\u2013252 (1977). https:\/\/doi.org\/10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"key":"24_CR8","doi-asserted-by":"publisher","unstructured":"Ehlers, R.: Formal verification of piece-wise linear feed-forward neural networks. In: International Symposium on Automated Technology for Verification and Analysis, pp. 269\u2013286. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-68167-2_19","DOI":"10.1007\/978-3-319-68167-2_19"},{"key":"24_CR9","doi-asserted-by":"publisher","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: 2018 IEEE symposium on security and privacy (SP), pp. 3\u201318. IEEE (2018). https:\/\/doi.org\/10.1109\/SP.2018.00058","DOI":"10.1109\/SP.2018.00058"},{"key":"24_CR10","doi-asserted-by":"publisher","unstructured":"Geiger, A., Lenz, P., Urtasun, R.: Are we ready for autonomous driving? the kitti vision benchmark suite. In: 2012 IEEE Conference on Computer Vision and Pattern Recognition, pp. 3354\u20133361. IEEE (2012). https:\/\/doi.org\/10.1109\/CVPR.2012.6248074","DOI":"10.1109\/CVPR.2012.6248074"},{"key":"24_CR11","doi-asserted-by":"publisher","unstructured":"Goodfellow, I.J., Shlens, J., Szegedy, C.: Explaining and harnessing adversarial examples. arXiv preprint arXiv:1412.6572 (2014). https:\/\/doi.org\/10.48550\/arXiv.1412.6572","DOI":"10.48550\/arXiv.1412.6572"},{"key":"24_CR12","doi-asserted-by":"publisher","unstructured":"Gowal, S., et al.: On the effectiveness of interval bound propagation for training verifiably robust models. arXiv preprint arXiv:1810.12715 (2018). https:\/\/doi.org\/10.48550\/arXiv.1810.12715","DOI":"10.48550\/arXiv.1810.12715"},{"key":"24_CR13","unstructured":"Gurobi Optimization, LLC: Gurobi Optimizer Reference Manual (2023)"},{"key":"24_CR14","doi-asserted-by":"publisher","unstructured":"He, K., Gkioxari, G., Doll\u00e1r, P., Girshick, R.: Mask r-CNN. In: Proceedings of the IEEE International Conference on Computer Vision, pp. 2961\u20132969 (2017). https:\/\/doi.org\/10.1109\/ICCV.2017.322","DOI":"10.1109\/ICCV.2017.322"},{"key":"24_CR15","doi-asserted-by":"publisher","unstructured":"Katz, G., Barrett, C., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: An efficient smt solver for verifying deep neural networks. In: International conference on computer aided verification, pp. 97\u2013117. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_5","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"24_CR16","doi-asserted-by":"publisher","unstructured":"Katz, G., et\u00a0al.: The marabou framework for verification and analysis of deep neural networks. In: International Conference on Computer Aided Verification, pp. 443\u2013452. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_26","DOI":"10.1007\/978-3-030-25540-4_26"},{"key":"24_CR17","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1016\/j.media.2017.07.005","volume":"42","author":"G Litjens","year":"2017","unstructured":"Litjens, G., et al.: A survey on deep learning in medical image analysis. Med. Image Anal. 42, 60\u201388 (2017). https:\/\/doi.org\/10.1016\/j.media.2017.07.005","journal-title":"Med. Image Anal."},{"key":"24_CR18","doi-asserted-by":"publisher","unstructured":"Lomuscio, A., Maganti, L.: An approach to reachability analysis for feed-forward ReLU neural networks. arXiv preprint arXiv:1706.07351 (2017). https:\/\/doi.org\/10.48550\/arXiv.1706.07351","DOI":"10.48550\/arXiv.1706.07351"},{"key":"24_CR19","doi-asserted-by":"publisher","unstructured":"Long, J., Shelhamer, E., Darrell, T.: Fully convolutional networks for semantic segmentation. In: Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition, pp. 3431\u20133440 (2015). https:\/\/doi.org\/10.1109\/CVPR.2015.7298965","DOI":"10.1109\/CVPR.2015.7298965"},{"key":"24_CR20","doi-asserted-by":"publisher","unstructured":"Madry, A., Makelov, A., Schmidt, L., Tsipras, D., Vladu, A.: Towards deep learning models resistant to adversarial attacks. arXiv preprint arXiv:1706.06083 (2017). https:\/\/doi.org\/10.48550\/arXiv.1706.06083","DOI":"10.48550\/arXiv.1706.06083"},{"key":"24_CR21","doi-asserted-by":"publisher","unstructured":"M\u00fcller, M.N., Makarchuk, G., Singh, G., P\u00fcschel, M., Vechev, M.: Prima: general and precise neural network certification via scalable convex hull approximations. Proc. ACM Programm. Lang. 6(POPL), 1\u201333 (2022). https:\/\/doi.org\/10.1145\/3498704","DOI":"10.1145\/3498704"},{"key":"24_CR22","doi-asserted-by":"publisher","unstructured":"Ronneberger, O., Fischer, P., Brox, T.: U-net: convolutional networks for biomedical image segmentation. In: International Conference on Medical image computing and computer-assisted intervention. pp. 234\u2013241. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-24574-4_28","DOI":"10.1007\/978-3-319-24574-4_28"},{"key":"24_CR23","doi-asserted-by":"publisher","unstructured":"Singh, G., Gehr, T., Mirman, M., P\u00fcschel, M., Vechev, M.: Fast and effective robustness certification. Adv. Neural Inform. Process. Syst. 31 (2018). https:\/\/doi.org\/10.5555\/3327546.3327739","DOI":"10.5555\/3327546.3327739"},{"key":"24_CR24","doi-asserted-by":"publisher","unstructured":"Singh, G., Gehr, T., P\u00fcschel, M., Vechev, M.: An abstract domain for certifying neural networks. Proc. ACM Programm. Lang. 3(POPL), 1\u201330 (2019). https:\/\/doi.org\/10.1145\/3290354","DOI":"10.1145\/3290354"},{"key":"24_CR25","doi-asserted-by":"publisher","unstructured":"Tjeng, V., Xiao, K., Tedrake, R.: Evaluating robustness of neural networks with mixed integer programming. arXiv preprint arXiv:1711.07356 (2017). https:\/\/doi.org\/10.48550\/arXiv.1711.07356","DOI":"10.48550\/arXiv.1711.07356"},{"key":"24_CR26","doi-asserted-by":"publisher","unstructured":"Tran, H.D., Bak, S., Xiang, W., Johnson, T.T.: Verification of deep convolutional neural networks using imagestars. In: International conference on computer aided verification, pp. 18\u201342. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_2","DOI":"10.1007\/978-3-030-53288-8_2"},{"key":"24_CR27","doi-asserted-by":"publisher","unstructured":"Tran, H.D., et al.: StarV: a qualitative and quantitative verification tool for learning-enabled systems. In: International Conference on Computer Aided Verification, pp. 376\u2013394. Springer (2025). https:\/\/doi.org\/10.1007\/978-3-031-98679_17","DOI":"10.1007\/978-3-031-98679_17"},{"key":"24_CR28","doi-asserted-by":"publisher","unstructured":"Tran, H.D., Manzanas\u00a0Lopez, D., Musau, P., Yang, X., Nguyen, L.V., Xiang, W., Johnson, T.T.: Star-based reachability analysis of deep neural networks. In: International Symposium on Formal Methods, pp. 670\u2013686. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-30942-8_39","DOI":"10.1007\/978-3-030-30942-8_39"},{"key":"24_CR29","doi-asserted-by":"publisher","unstructured":"Tran, H.D., et al.: Johnson, T.T.: Robustness verification of semantic segmentation neural networks using relaxed reachability. In: International Conference on Computer Aided Verification, pp. 263\u2013286. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_12","DOI":"10.1007\/978-3-030-81685-8_12"},{"key":"24_CR30","doi-asserted-by":"publisher","unstructured":"Tran, H.D., et al.: Nnv: the neural network verification tool for deep neural networks and learning-enabled cyber-physical systems. In: International Conference on Computer Aided Verification, pp. 3\u201317. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_1","DOI":"10.1007\/978-3-030-53288-8_1"},{"key":"24_CR31","doi-asserted-by":"publisher","first-page":"29909","DOI":"10.5555\/3540261.3542550","volume":"34","author":"S Wang","year":"2021","unstructured":"Wang, S., et al.: Beta-crown: efficient bound propagation with per-neuron split constraints for neural network robustness verification. Adv. Neural. Inf. Process. Syst. 34, 29909\u201329921 (2021). https:\/\/doi.org\/10.5555\/3540261.3542550","journal-title":"Adv. Neural. Inf. Process. Syst."},{"key":"24_CR32","doi-asserted-by":"publisher","unstructured":"Xie, C., Wang, J., Zhang, Z., Zhou, Y., Xie, L., Yuille, A.: Adversarial examples for semantic segmentation and object detection. In: Proceedings of the IEEE International Conference on Computer Vision, pp. 1369\u20131378 (2017). https:\/\/doi.org\/10.1109\/ICCV.2017.153","DOI":"10.1109\/ICCV.2017.153"},{"key":"24_CR33","doi-asserted-by":"publisher","first-page":"1129","DOI":"10.5555\/3495724.3495820","volume":"33","author":"K Xu","year":"2020","unstructured":"Xu, K., et al.: Automatic perturbation analysis for scalable certified robustness and beyond. Adv. Neural. Inf. Process. Syst. 33, 1129\u20131141 (2020). https:\/\/doi.org\/10.5555\/3495724.3495820","journal-title":"Adv. Neural. Inf. Process. Syst."},{"key":"24_CR34","doi-asserted-by":"publisher","unstructured":"Zhang, H., Weng, T.W., Chen, P.Y., Hsieh, C.J., Daniel, L.: Efficient neural network robustness certification with general activation functions. Adv. Neural Inform. Process. Syst. 31 (2018). https:\/\/doi.org\/10.5555\/3327345.3327402","DOI":"10.5555\/3327345.3327402"},{"key":"24_CR35","doi-asserted-by":"publisher","unstructured":"Zhao, H., Shi, J., Qi, X., Wang, X., Jia, J.: Pyramid scene parsing network. In: Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition, pp. 2881\u20132890 (2017). https:\/\/doi.org\/10.1109\/CVPR.2017.660","DOI":"10.1109\/CVPR.2017.660"}],"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-032-32526-6_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:45:20Z","timestamp":1784796320000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-32526-6_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032325259","9783032325266"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-32526-6_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"24 July 2026","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","label":"Disclosure of Interests","group":{"name":"EthicsHeading","label":"Ethics"}},{"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":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 July 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 July 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"38","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.floc26.org\/program","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}