{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,13]],"date-time":"2026-03-13T06:44:05Z","timestamp":1773384245555,"version":"3.50.1"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030921231","type":"print"},{"value":"9783030921248","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-92124-8_26","type":"book-chapter","created":{"date-parts":[[2021,12,2]],"date-time":"2021-12-02T17:18:47Z","timestamp":1638465527000},"page":"463-480","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["OSIP: Tightened Bound Propagation for\u00a0the\u00a0Verification of\u00a0ReLU Neural Networks"],"prefix":"10.1007","author":[{"given":"Vahid","family":"Hashemi","sequence":"first","affiliation":[]},{"given":"Panagiotis","family":"Kouvaros","sequence":"additional","affiliation":[]},{"given":"Alessio","family":"Lomuscio","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,12,3]]},"reference":[{"issue":"1","key":"26_CR1","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10107-020-01474-5","volume":"183","author":"R Anderson","year":"2020","unstructured":"Anderson, R., Huchette, J., Ma, W., Tjandraatmadja, C., Vielma, J.P.: Strong mixed-integer programming formulations for trained neural networks. Math. Progr. 183(1), 3\u201339 (2020). https:\/\/doi.org\/10.1007\/s10107-020-01474-5","journal-title":"Math. Progr."},{"key":"26_CR2","unstructured":"Bastani, O., Ioannou, Y., Lampropoulos, L., Vytiniotis, D., Nori, A.V., Criminisi, A.: Measuring neural net robustness with constraints. In: Proceedings of the 30th International Conference on Neural Information Processing Systems (NIPS16), pp. 2613\u20132621 (2016)"},{"key":"26_CR3","doi-asserted-by":"crossref","unstructured":"Battern, B., Kouvaros, P., Lomuscio, A., Zheng, Y.: Efficient neural network verification via layer-based semidefinite relaxations and linear cuts. In: International Joint Conference on Artificial Intelligence (IJCAI21), pp. 2184\u20132190. ijcai.org (2021)","DOI":"10.24963\/ijcai.2021\/301"},{"key":"26_CR4","doi-asserted-by":"crossref","unstructured":"Botoeva, E., Kouvaros, P., Kronqvist, J., Lomuscio, A., Misener, R.: Efficient verification of neural networks via dependency analysis. In: Proceedings of the 34th AAAI Conference on Artificial Intelligence (AAAI20). AAAI Press (2020)","DOI":"10.1609\/aaai.v34i04.5729"},{"key":"26_CR5","doi-asserted-by":"crossref","unstructured":"Chen, X., Ma, H., Wan, J., Li, B., Xia, T.: Multi-view 3D object detection network for autonomous driving. In: Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition, pp. 1907\u20131915 (2017)","DOI":"10.1109\/CVPR.2017.691"},{"key":"26_CR6","doi-asserted-by":"publisher","unstructured":"Cheng, C.-H., N\u00fchrenberg, G., Ruess, H.: Maximum resilience of artificial neural networks. In: D\u2019Souza, D., Narayan Kumar, K. (eds.) ATVA 2017. LNCS, vol. 10482, pp. 251\u2013268. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68167-2_18","DOI":"10.1007\/978-3-319-68167-2_18"},{"key":"26_CR7","unstructured":"Dathathri, S., et al.: Enabling certification of verification-agnostic networks via memory-efficient semidefinite programming. In: NeurIPS20 (2020)"},{"key":"26_CR8","unstructured":"Dvijotham, K., Stanforth, R., Gowal, S., Mann, T., Kohli, P.: A dual approach to scalable verification of deep networks. In: UAI. vol. 1, p. 2 (2018)"},{"key":"26_CR9","doi-asserted-by":"publisher","unstructured":"Ehlers, R.: In: D\u2019Souza, D., Narayan Kumar, K. (eds.) ATVA 2017. LNCS, vol. 10482, pp. 269\u2013286. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68167-2_19","DOI":"10.1007\/978-3-319-68167-2_19"},{"key":"26_CR10","doi-asserted-by":"crossref","unstructured":"Fazlyab, M., Morari, M., Pappas, G.J.: Safety verification and robustness analysis of neural networks via quadratic constraints and semidefinite programming (2019). arXiv preprint arXiv:1903.01287","DOI":"10.1109\/TAC.2020.3046193"},{"issue":"3","key":"26_CR11","doi-asserted-by":"publisher","first-page":"296","DOI":"10.1007\/s10601-018-9285-6","volume":"23","author":"M Fischetti","year":"2018","unstructured":"Fischetti, M., Jo, J.: Deep neural networks and mixed integer linear optimization. Constraints 23(3), 296\u2013309 (2018). https:\/\/doi.org\/10.1007\/s10601-018-9285-6","journal-title":"Constraints"},{"key":"26_CR12","unstructured":"Goodfellow, I., Shlens, J., Szegedy, C.: Explaining and harnessing adversarial examples (2014). arXiv preprint arXiv:1412.6572"},{"key":"26_CR13","doi-asserted-by":"crossref","unstructured":"Henriksen, P., Lomuscio, A.: DEEPSPLIT: an efficient splitting method for neural network verification via indirect effect analysis. In: Proceedings of the 30th International Joint Conference on Artificial Intelligence (IJCAI21), pp. 2549\u20132555. ijcai.org (2021)","DOI":"10.24963\/ijcai.2021\/351"},{"key":"26_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-53288-8_1","volume-title":"Computer Aided Verification","author":"H-D Tran","year":"2020","unstructured":"Tran, H.-D., et al.: NNV: the neural network verification tool for deep neural networks and learning-enabled cyber-physical systems. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 3\u201317. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_1"},{"key":"26_CR15","doi-asserted-by":"publisher","unstructured":"Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety verification of deep neural networks. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 3\u201329. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_1","DOI":"10.1007\/978-3-319-63387-9_1"},{"key":"26_CR16","doi-asserted-by":"crossref","unstructured":"Julian, K., Lopez, J., Brush, J., Owen, M., Kochenderfer, M.: Policy compression for aircraft collision avoidance systems. In: DASC16, pp. 1\u201310 (2016)","DOI":"10.1109\/DASC.2016.7778091"},{"key":"26_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":"26_CR18","doi-asserted-by":"crossref","unstructured":"Katz, G., et al.: The marabou framework for verification and analysis of deep neural networks. In: Proceedings of the 31st International Conference on Computer Aided Verification (CAV19), pp. 443\u2013452 (2019)","DOI":"10.1007\/978-3-030-25540-4_26"},{"key":"26_CR19","doi-asserted-by":"crossref","unstructured":"Kouvaros, P., Lomuscio, A.: Towards scalable complete verification of relu neural networks via dependency-based branching. In: International Joint Conference on Artificial Intelligence (IJCAI21), pp. 2643\u20132650. ijcai.org (2021)","DOI":"10.24963\/ijcai.2021\/364"},{"key":"26_CR20","unstructured":"LeCun, Y., Cortes, C., Burges, C.J.: The MNIST database of handwritten digits (1998)"},{"key":"26_CR21","unstructured":"Lomuscio, A., Maganti, L.: An approach to reachability analysis for feed-forward relu neural networks. CoRR abs\/1706.07351 (2017)"},{"key":"26_CR22","unstructured":"Henriksen, P., Lomuscio, A.: Efficient neural network verification via adaptive refinement and adversarial search. In: ECAI20 (2020)"},{"key":"26_CR23","unstructured":"Raghunathan, A., Steinhardt, J., Liang, P.: Semidefinite relaxations for certifying robustness to adversarial examples. In: Advances in Neural Information Processing Systems 31, pp. 10877\u201310887. Curran Associates, Inc. (2018)"},{"key":"26_CR24","unstructured":"Salman, H., Yang, G., Zhang, H., Hsieh, C., Zhang, P.: A convex relaxation barrier to tight robustness verification of neural networks. In: Advances in Neural Information Processing Systems 32, pp. 9835\u20139846. Curran Associates, Inc. (2019)"},{"key":"26_CR25","unstructured":"Simonyan, K., Zisserman, A.: Very deep convolutional networks for large-scale image recognition (2014). arXiv preprint arXiv:1409.1556"},{"key":"26_CR26","doi-asserted-by":"crossref","unstructured":"Singh, G., Gehr, T., P\u00fcschel, M., Vechev, P.: An abstract domain for certifying neural networks. In: Proceedings of the ACM on Programming Languages 3(POPL), 41 (2019)","DOI":"10.1145\/3290354"},{"key":"26_CR27","doi-asserted-by":"crossref","unstructured":"Stallkamp, J., Schlipsing, M., Salmen, J., Igel, C.: The german traffic sign recognition benchmark: a multi-class classification competition. In: The 2011 International Joint Conference on Neural Networks, pp. 1453\u20131460. IEEE (2011)","DOI":"10.1109\/IJCNN.2011.6033395"},{"key":"26_CR28","unstructured":"Tjandraatmadja, C., Anderson, R., Huchette, J., Ma, W., Patel, K., Vielma, J.: The convex relaxation barrier, revisited: tightened single-neuron relaxations for neural network verification. In: NeurIPS20 (2020)"},{"key":"26_CR29","unstructured":"Tjeng, V., Xiao, K.Y., Tedrake, R.: Evaluating robustness of neural networks with mixed integer programming. In: Proceedings of the 7th International Conference on Learning Representations (ICLR19) (2019)"},{"key":"26_CR30","unstructured":"VNN-COMP: Vefication of neural networks competition (2020). https:\/\/sites.google.com\/view\/vnn20\/vnncomp"},{"key":"26_CR31","unstructured":"Wang, S., Pei, K., Whitehouse, J., Yang, J., Jana, S.: Efficient formal safety analysis of neural networks. In: Proceedings of the 31st Annual Conference on Neural Information Processing Systems 2018 (NeurIPS18), pp. 6369\u20136379 (2018)"},{"key":"26_CR32","unstructured":"Wang, S., Pei, K., Whitehouse, J., Yang, J., Jana, S.: Formal security analysis of neural networks using symbolic intervals. In: Proceedings of the 27th USENIX Security Symposium, (USENIX18), pp. 1599\u20131614 (2018)"},{"key":"26_CR33","unstructured":"Weng, T., et al.: Towards fast computation of certified robustness for relu networks (2018). arXiv preprint arXiv:1804.09699"},{"key":"26_CR34","unstructured":"Wong, E., Kolter, J.: Provable defenses against adversarial examples via the convex outer adversarial polytope (2017). arXiv preprint arXiv:1711.00851"},{"key":"26_CR35","unstructured":"Wong, E., Schmidt, F., Metzen, J., Kolter, J.: Scaling provable adversarial defenses. In: Proceedings of the 32nd Conference on Neural Information Processing Systems (NeurIPS18) (2018)"},{"issue":"11","key":"26_CR36","doi-asserted-by":"publisher","first-page":"5777","DOI":"10.1109\/TNNLS.2018.2808470","volume":"29","author":"W Xiang","year":"2018","unstructured":"Xiang, W., Tran, H., Johnson, T.: Output reachable set estimation and verification for multilayer neural networks. IEEE Trans. Neural Netw. Learn. Syst. 29(11), 5777\u20135783 (2018)","journal-title":"IEEE Trans. Neural Netw. Learn. Syst."},{"key":"26_CR37","unstructured":"Zhang, H., Weng, T., Chen, P., Hsieh, C., Daniel, L.: Efficient neural network robustness certification with general activation functions. In: Proceedings of the 31st Annual Conference on Neural Information Processing Systems 2018 (NeurIPS2018), pp. 4944\u20134953. Curran Associates, Inc. (2018)"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-92124-8_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,2]],"date-time":"2021-12-02T17:22:15Z","timestamp":1638465735000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-92124-8_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030921231","9783030921248"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-92124-8_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"3 December 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SEFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Software Engineering and Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 December 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 December 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sefm2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/sefm-conference.github.io\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-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":"86","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":"22","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":"4","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":"26% - 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","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":"6.5","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)"}}]}}