{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T08:18:04Z","timestamp":1743149884620,"version":"3.40.3"},"publisher-location":"Cham","reference-count":46,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031453281"},{"type":"electronic","value":"9783031453298"}],"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:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"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":[[2023]]},"DOI":"10.1007\/978-3-031-45329-8_20","type":"book-chapter","created":{"date-parts":[[2023,10,21]],"date-time":"2023-10-21T18:02:40Z","timestamp":1697911360000},"page":"422-443","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Using Counterexamples to\u00a0Improve Robustness Verification in\u00a0Neural Networks"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6173-3959","authenticated-orcid":false,"given":"Mohammad","family":"Afzal","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-7755-2006","authenticated-orcid":false,"given":"Ashutosh","family":"Gupta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2471-5997","authenticated-orcid":false,"given":"S.","family":"Akshay","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,10,22]]},"reference":[{"key":"20_CR1","unstructured":"Bojarski, M., et al.: End to end learning for self-driving cars. Volume abs\/1604.07316 (2016)"},{"key":"20_CR2","doi-asserted-by":"publisher","first-page":"47","DOI":"10.2478\/v10136-012-0031-x","volume":"11","author":"F Amato","year":"2013","unstructured":"Amato, F., L\u00f3pez, A., Pe\u00f1a-M\u00e9ndez, E.M., Va\u0148hara, P., Hampl, A., Havel, J.: Artificial neural networks in medical diagnosis. J. Appl. Biomed. 11, 47\u201358 (2013)","journal-title":"J. Appl. Biomed."},{"issue":"6","key":"20_CR3","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1109\/MSP.2012.2205597","volume":"29","author":"G Hinton","year":"2012","unstructured":"Hinton, G., et al.: Deep neural networks for acoustic modeling in speech recognition: the shared views of four research groups. IEEE Sig. Process. Mag. 29(6), 82\u201397 (2012)","journal-title":"IEEE Sig. Process. Mag."},{"key":"20_CR4","unstructured":"Goodfellow, I.J., Shlens, J., Szegedy, C.: Explaining and harnessing adversarial examples. In: Bengio, Y., LeCun, Y. (eds.) 3rd International Conference on Learning Representations, ICLR 2015, San Diego, CA, USA, 7\u20139 May 2015, Conference Track Proceedings (2015)"},{"key":"20_CR5","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/s10703-021-00363-7","volume":"60","author":"G Katz","year":"2021","unstructured":"Katz, G., Barrett, C., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: a calculus for reasoning about deep neural networks. Formal Methods Syst. Des. 60, 87\u2013116 (2021). https:\/\/doi.org\/10.1007\/s10703-021-00363-7","journal-title":"Formal Methods Syst. Des."},{"key":"20_CR6","unstructured":"Lomuscio, A., Maganti, L.: An approach to reachability analysis for feed-forward ReLU neural networks. CoRR, abs\/1706.07351 (2017)"},{"issue":"3","key":"20_CR7","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 Int. J. 23(3), 296\u2013309 (2018). https:\/\/doi.org\/10.1007\/s10601-018-9285-6","journal-title":"Constraints Int. J."},{"key":"20_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-319-77935-5_9","volume-title":"NASA Formal Methods","author":"S Dutta","year":"2018","unstructured":"Dutta, S., Jha, S., Sankaranarayanan, S., Tiwari, A.: Output range analysis for deep feedforward neural networks. In: Dutle, A., Mu\u00f1oz, C., Narkawicz, A. (eds.) NFM 2018. LNCS, vol. 10811, pp. 121\u2013138. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-77935-5_9"},{"key":"20_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-319-68167-2_18","volume-title":"Automated Technology for Verification and Analysis","author":"C-H Cheng","year":"2017","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"},{"key":"20_CR10","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":"20_CR11","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":"20_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/978-3-319-68167-2_19","volume-title":"Automated Technology for Verification and Analysis","author":"R Ehlers","year":"2017","unstructured":"Ehlers, R.: Formal verification of piece-wise linear feed-forward neural networks. 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"},{"key":"20_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-63387-9_1","volume-title":"Computer Aided Verification","author":"X Huang","year":"2017","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"},{"key":"20_CR14","unstructured":"Wang, S., et al.: Beta-CROWN: efficient bound propagation with per-neuron split constraints for neural network robustness verification. In: Advances in Neural Information Processing Systems, vol. 34, pp. 29909\u201329921 (2021)"},{"key":"20_CR15","unstructured":"Xu, K., et al.: Fast and complete: enabling complete neural network verification with rapid and massively parallel incomplete verifiers. CoRR, abs\/2011.13824 (2020)"},{"key":"20_CR16","unstructured":"Zhang, H., et al.: General cutting planes for bound-propagation-based neural network verification. CoRR, abs\/2208.05740 (2022)"},{"key":"20_CR17","unstructured":"Dvijotham, K., Stanforth, R., Gowal, S., Mann, T.A., Kohli, P.: A dual approach to scalable verification of deep networks. In: UAI, vol. 1, p. 3 (2018)"},{"key":"20_CR18","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: 2018 IEEE Symposium on Security and Privacy, SP 2018, Proceedings, San Francisco, California, USA, 21\u201323 May 2018, pp. 3\u201318. IEEE Computer Society (2018)","DOI":"10.1109\/SP.2018.00058"},{"key":"20_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, Montr\u00e9al, Canada, 3\u20138 December 2018, pp. 10825\u201310836 (2018)"},{"key":"20_CR20","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, May 6\u20139 2019. OpenReview.net (2019)"},{"key":"20_CR21","unstructured":"Weng, L., et al.: Towards fast computation of certified robustness for ReLU networks. In: International Conference on Machine Learning, pp. 5276\u20135285. PMLR (2018)"},{"key":"20_CR22","unstructured":"Wong, E., Kolter, Z.: Provable defenses against adversarial examples via the convex outer adversarial polytope. In: International Conference on Machine Learning, pp. 5286\u20135295. PMLR (2018)"},{"key":"20_CR23","unstructured":"Zhang, H., Weng, T.-W., Chen, P.-Y., Hsieh, C.-J., Daniel, L.: Efficient neural network robustness certification with general activation functions. In: Advances in Neural Information Processing Systems, vol. 31 (2018)"},{"issue":"POPL","key":"20_CR24","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3290354","volume":"3","author":"G Singh","year":"2019","unstructured":"Singh, G., Gehr, T., P\u00fcschel, M., Vechev, M.: An abstract domain for certifying neural networks. Proc. ACM Program. Lang. 3(POPL), 1\u201330 (2019)","journal-title":"Proc. ACM Program. Lang."},{"key":"20_CR25","unstructured":"Wang, S., Pei, K., Whitehouse, J., Yang, J., Jana, S.: Formal security analysis of neural networks using symbolic intervals. In: 27th USENIX Security Symposium (USENIX Security 2018), pp. 1599\u20131614 (2018)"},{"key":"20_CR26","unstructured":"Wang, S., Pei, K., Whitehouse, J., Yang, J., Jana, S.: Efficient formal safety analysis of neural networks. In: Advances in Neural Information Processing Systems, pp. 6367\u20136377 (2018)"},{"key":"20_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-030-53288-8_3","volume-title":"Computer Aided Verification","author":"YY Elboher","year":"2020","unstructured":"Elboher, Y.Y., Gottschlich, J., Katz, G.: An abstraction-based framework for neural network verification. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 43\u201365. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_3"},{"key":"20_CR28","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":"20_CR29","unstructured":"Lin, X., Zhu, H., Samanta, R., Jagannathan, S.: ART: abstraction refinement-guided training for provably correct neural networks. In: 2020 Formal Methods in Computer Aided Design, FMCAD 2020, Haifa, Israel, 21\u201324 September 2020, pp. 148\u2013157. IEEE (2020)"},{"issue":"2","key":"20_CR30","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1016\/j.trb.2006.02.002","volume":"41","author":"B Bixby","year":"2007","unstructured":"Bixby, B.: The gurobi optimizer. Transp. Res. Part B 41(2), 159\u2013178 (2007)","journal-title":"Transp. Res. Part B"},{"key":"20_CR31","unstructured":"Singh, G., Ganvir, R., P\u00fcschel, M., Vechev, M.: Beyond the single neuron convex barrier for neural network certification. In: Advances in Neural Information Processing Systems, vol. 32 (2019)"},{"key":"20_CR32","doi-asserted-by":"crossref","unstructured":"Dong, Y., et al.: Boosting adversarial attacks with momentum. In: Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition, pp. 9185\u20139193 (2018)","DOI":"10.1109\/CVPR.2018.00957"},{"key":"20_CR33","unstructured":"$$\\alpha \\beta $$-CROWN (2021). https:\/\/github.com\/huanzhang12\/alpha-beta-CROWN"},{"key":"20_CR34","first-page":"1","volume":"21","author":"R Bunel","year":"2020","unstructured":"Bunel, R., Mudigonda, P., Turkaslan, I., Torr, P., Lu, J., Kohli, P.: Branch and bound for piecewise linear neural network verification. J. Mach. Learn. Res. 21, 1\u201339 (2020)","journal-title":"J. Mach. Learn. Res."},{"key":"20_CR35","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proceedings of the 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 84\u201396 (1978)","DOI":"10.1145\/512760.512770"},{"key":"20_CR36","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 the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"20_CR37","unstructured":"Tjeng, V., Xiao, K.Y., Tedrake, R.: Evaluating robustness of neural networks with mixed integer programming. In: 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, 6\u20139 May 2019. OpenReview.net (2019)"},{"key":"20_CR38","unstructured":"Zhang, H., et al.: A branch and bound framework for stronger adversarial attacks of ReLU networks. In: International Conference on Machine Learning, pp. 26591\u201326604. PMLR (2022)"},{"key":"20_CR39","unstructured":"Bunel, R.R., Turkaslan, I., Torr, P., Kohli, P., Mudigonda, P.K.: A unified view of piecewise linear neural network verification. In: Advances in Neural Information Processing Systems, vol. 31 (2018)"},{"key":"20_CR40","unstructured":"Bunel, R., et al.: Lagrangian decomposition for neural network verification. In: Conference on Uncertainty in Artificial Intelligence, pp. 370\u2013379. PMLR (2020)"},{"key":"20_CR41","unstructured":"De Palma, A., Behl, H.S., Bunel, R., Torr, P., Kumar, M.P.: Scaling the convex barrier with active sets. In: Proceedings of the ICLR 2021 Conference. Open Review (2021)"},{"key":"20_CR42","unstructured":"De Palma, A., Behl, H.S., Bunel, R., Torr, P.H.S., Kumar, M.P.: Scaling the convex barrier with sparse dual algorithms. CoRR, abs\/2101.05844 (2021)"},{"key":"20_CR43","unstructured":"De Palma, A., et al.: Improved branch and bound for neural network verification via lagrangian decomposition. CoRR, abs\/2104.06718 (2021)"},{"issue":"6","key":"20_CR44","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1109\/MSP.2012.2211477","volume":"29","author":"L Deng","year":"2012","unstructured":"Deng, L.: The MNIST database of handwritten digit images for machine learning research [best of the web]. IEEE Sig. Process. Mag. 29(6), 141\u2013142 (2012)","journal-title":"IEEE Sig. Process. Mag."},{"key":"20_CR45","unstructured":"Mirman, M., Gehr, T., Vechev, M.: Differentiable abstract interpretation for provably robust neural networks. In: International Conference on Machine Learning, pp. 3578\u20133586. PMLR (2018)"},{"key":"20_CR46","unstructured":"Brain, M., Davenport, J.H., Griggio, A.: Benchmarking solvers, SAT-style. In: SC$$^2$$@ ISSAC (2017)"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-45329-8_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,10,21]],"date-time":"2023-10-21T18:05:14Z","timestamp":1697911514000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-45329-8_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031453281","9783031453298"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-45329-8_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"22 October 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ATVA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Automated Technology for Verification and Analysis","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Singapore","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Singapore","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":"24 October 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 October 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"atva2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/atva-conference.org\/2023\/","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":"115","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":"30","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":"0","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.05","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","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)"}},{"value":"7 tool papers","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}