{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,12]],"date-time":"2025-12-12T13:06:43Z","timestamp":1765544803655,"version":"3.40.3"},"publisher-location":"Cham","reference-count":71,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030816841"},{"type":"electronic","value":"9783030816858"}],"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:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,7,15]],"date-time":"2021-07-15T00:00:00Z","timestamp":1626307200000},"content-version":"vor","delay-in-days":195,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Verifying and explaining the behavior of neural networks is becoming increasingly important, especially when they are deployed in safety-critical applications. In this paper, we study verification and interpretability problems for Binarized Neural Networks (BNNs), the 1-bit quantization of general real-numbered neural networks. Our approach is to encode BNNs into Binary Decision Diagrams (BDDs), which is done by exploiting the internal structure of the BNNs. In particular, we translate the input-output relation of blocks in BNNs to cardinality constraints which are in turn encoded by BDDs. Based on the encoding, we develop a quantitative framework for BNNs where precise and comprehensive analysis of BNNs can be performed. We demonstrate the application of our framework by providing quantitative robustness analysis and interpretability for BNNs. We implement a prototype tool and carry out extensive experiments, confirming the effectiveness and efficiency of our approach.<\/jats:p>","DOI":"10.1007\/978-3-030-81685-8_8","type":"book-chapter","created":{"date-parts":[[2021,7,17]],"date-time":"2021-07-17T00:02:35Z","timestamp":1626480155000},"page":"175-200","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":25,"title":["BDD4BNN: A BDD-Based Quantitative Analysis Framework for Binarized Neural Networks"],"prefix":"10.1007","author":[{"given":"Yedi","family":"Zhang","sequence":"first","affiliation":[]},{"given":"Zhe","family":"Zhao","sequence":"additional","affiliation":[]},{"given":"Guangke","family":"Chen","sequence":"additional","affiliation":[]},{"given":"Fu","family":"Song","sequence":"additional","affiliation":[]},{"given":"Taolue","family":"Chen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,7,15]]},"reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"Amir, G., Wu, H., Barrett, C.W., Katz, G.: An SMT-based approach for verifying binarized neural networks. CoRR abs\/2011.02948 (2020)","DOI":"10.26226\/morressier.604907f41a80aac83ca25cda"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Anderson, G., Pailoor, S., Dillig, I., Chaudhuri, S.: Optimization and abstraction: a synergistic approach for analyzing neural network robustness. In: PLDI, pp. 731\u2013744 (2019)","DOI":"10.1145\/3314221.3314614"},{"key":"8_CR3","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":"8_CR4","unstructured":"Baidu: Apollo (2021). https:\/\/apollo.auto"},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"Baluta, T., Chua, Z.L., Meel, K.S., Saxena, P.: Scalable quantitative verification for deep neural networks. CoRR abs\/2002.06864 (2020)","DOI":"10.1109\/ICSE-Companion52605.2021.00115"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Baluta, T., Shen, S., Shinde, S., Meel, K.S., Saxena, P.: Quantitative verification of neural networks and its security applications. In: CCS, pp. 1249\u20131264 (2019)","DOI":"10.1145\/3319535.3354245"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1007\/978-3-030-51074-9_2","volume-title":"Automated Reasoning","author":"M Baranowski","year":"2020","unstructured":"Baranowski, M., He, S., Lechner, M., Nguyen, T.S., Rakamari\u0107, Z.: An SMT theory of fixed-point arithmetic. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNCS (LNAI), vol. 12166, pp. 13\u201331. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-51074-9_2"},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1007\/3-540-36577-X_28","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C Bartzis","year":"2003","unstructured":"Bartzis, C., Bultan, T.: Construction of efficient BDDs for bounded arithmetic constraints. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 394\u2013408. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-36577-X_28"},{"issue":"8","key":"8_CR9","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"RE Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. 35(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"key":"8_CR10","first-page":"42:1","volume":"21","author":"R Bunel","year":"2020","unstructured":"Bunel, R., Lu, J., Turkaslan, I., Torr, P.H.S., Kohli, P., Kumar, M.P.: Branch and bound for piecewise linear neural network verification. J. Mach. Learn. Res. 21, 42:1-42:39 (2020)","journal-title":"J. Mach. Learn. Res."},{"key":"8_CR11","unstructured":"Chen, G., et al.: Who is real Bob? Adversarial attacks on speaker recognition systems. CoRR abs\/1911.01840 (2019)"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-030-03592-1_16","volume-title":"Verified Software. Theories, Tools, and Experiments","author":"C-H Cheng","year":"2018","unstructured":"Cheng, C.-H., N\u00fchrenberg, G., Huang, C.-H., Ruess, H.: Verification of binarized neural networks via inter-neuron factoring. In: Piskac, R., R\u00fcmmer, P. (eds.) VSTTE 2018. LNCS, vol. 11294, pp. 279\u2013290. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03592-1_16"},{"key":"8_CR13","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":"8_CR14","unstructured":"Duan, Y., Zhao, Z., Bu, L., Song, F.: Things you may not know about adversarial example: a black-box adversarial image attack. CoRR abs\/1905.07672 (2019)"},{"key":"8_CR15","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":"8_CR16","unstructured":"Dvijotham, K., Stanforth, R., Gowal, S., Mann, T.A., Kohli, P.: A dual approach to scalable verification of deep networks. In: UAI, pp. 550\u2013559 (2018)"},{"key":"8_CR17","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":"8_CR18","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":"8_CR19","unstructured":"Frosst, N., Hinton, G.E.: Distilling a neural network into a soft decision tree. In: Proceedings of the 1st International Workshop on Comprehensibility and Explanation in AI and ML (2017)"},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"Gehr, T., Mirman, M., Drachsler-Cohen, D., Tsankov, P., Chaudhuri, S., Vechev, M.T.: AI$$^2$$: safety and robustness certification of neural networks with abstract interpretation. In: S&P, pp. 3\u201318 (2018)","DOI":"10.1109\/SP.2018.00058"},{"key":"8_CR21","unstructured":"Ghosh, B., Basu, D., Meel, K.S.: Justicia: a stochastic SAT approach to formally verify fairness. CoRR abs\/2009.06516 (2020)"},{"key":"8_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/978-3-030-45237-7_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Giacobbe","year":"2020","unstructured":"Giacobbe, M., Henzinger, T.A., Lechner, M.: How many bits does it take to quantize your neural network? In: TACAS 2020. LNCS, vol. 12079, pp. 79\u201397. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45237-7_5"},{"key":"8_CR23","unstructured":"Gupta, S., Agrawal, A., Gopalakrishnan, K., Narayanan, P.: Deep learning with limited numerical precision. In: ICML, pp. 1737\u20131746 (2015)"},{"key":"8_CR24","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Lechner, M., \u017dikeli\u0107, D.: Scalable verification of quantized neural networks (technical report). arXiv preprint arXiv:2012.08185 (2020)","DOI":"10.1609\/aaai.v35i5.16496"},{"key":"8_CR25","doi-asserted-by":"publisher","first-page":"100270","DOI":"10.1016\/j.cosrev.2020.100270","volume":"37","author":"X Huang","year":"2020","unstructured":"Huang, X., et al.: A survey of safety and trustworthiness of deep neural networks: verification, testing, adversarial attack and defence, and interpretability. Comput. Sci. Rev. 37, 100270 (2020)","journal-title":"Comput. Sci. Rev."},{"key":"8_CR26","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":"8_CR27","unstructured":"Hubara, I., Courbariaux, M., Soudry, D., El-Yaniv, R., Bengio, Y.: Binarized neural networks. In: NeurIPS, pp. 4107\u20134115 (2016)"},{"key":"8_CR28","unstructured":"Jia, K., Rinard, M.: Efficient exact verification of binarized neural networks. In: NeurIPS (2020)"},{"key":"8_CR29","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1016\/j.tra.2016.09.010","volume":"94","author":"N Kalra","year":"2016","unstructured":"Kalra, N., Paddock, S.M.: Driving to safety: how many miles of driving would it take to demonstrate autonomous vehicle reliability? Transp. Res. Part A Policy Pract. 94, 182\u2013193 (2016)","journal-title":"Transp. Res. Part A Policy Pract."},{"key":"8_CR30","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":"8_CR31","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":"8_CR32","doi-asserted-by":"crossref","first-page":"512","DOI":"10.4271\/2019-01-0123","volume":"1","author":"P Koopman","year":"2019","unstructured":"Koopman, P., Osyk, B.: Safety argument considerations for public road testing of autonomous vehicles. SAE Int. J. Adv. Curr. Pract. Mobility 1, 512\u2013523 (2019)","journal-title":"SAE Int. J. Adv. Curr. Pract. Mobility"},{"key":"8_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"438","DOI":"10.1007\/978-3-319-94144-8_27","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2018","author":"S Korneev","year":"2018","unstructured":"Korneev, S., Narodytska, N., Pulina, L., Tacchella, A., Bjorner, N., Sagiv, M.: Constrained image generation using binarized neural networks with decision procedures. In: Beyersdorff, O., Wintersteiger, C.M. (eds.) SAT 2018. LNCS, vol. 10929, pp. 438\u2013449. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94144-8_27"},{"issue":"6","key":"8_CR34","doi-asserted-by":"publisher","first-page":"877","DOI":"10.1007\/s11265-017-1255-5","volume":"90","author":"J Kung","year":"2018","unstructured":"Kung, J., Zhang, D.C., van der Wal, G.S., Chai, S.M., Mukhopadhyay, S.: Efficient object detection using embedded binarized neural networks. J. Signal Process. Syst. 90(6), 877\u2013890 (2018)","journal-title":"J. Signal Process. Syst."},{"key":"8_CR35","unstructured":"LeCun, Y., Cortes, C.: MNIST handwritten digit database (2010)"},{"key":"8_CR36","unstructured":"Lei, Y., Chen, S., Fan, L., Song, F., Liu, Y.: Advanced evasion attacks and mitigations on practical ML-based phishing website classifiers. CoRR abs\/2004.06954 (2020)"},{"key":"8_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"296","DOI":"10.1007\/978-3-030-32304-2_15","volume-title":"Static Analysis","author":"J Li","year":"2019","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: Chang, B.-Y.E. (ed.) SAS 2019. LNCS, vol. 11822, pp. 296\u2013319. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-32304-2_15"},{"key":"8_CR38","doi-asserted-by":"crossref","unstructured":"Li, R., et al.: PRODeep: a platform for robustness verification of deep neural networks. In: FSE, pp. 1630\u20131634 (2020)","DOI":"10.1145\/3368089.3417918"},{"issue":"6","key":"8_CR39","doi-asserted-by":"publisher","first-page":"1365","DOI":"10.1007\/s11390-020-0546-7","volume":"35","author":"W Liu","year":"2020","unstructured":"Liu, W., Song, F., Zhang, T., Wang, J.: Verifying ReLU neural networks from a model checking perspective. J. Comput. Sci. Technol. 35(6), 1365\u20131381 (2020)","journal-title":"J. Comput. Sci. Technol."},{"key":"8_CR40","unstructured":"Lomuscio, A., Maganti, L.: An approach to reachability analysis for feed-forward ReLU neural networks. CoRR abs\/1706.07351 (2017)"},{"key":"8_CR41","unstructured":"McDanel, B., Teerapittayanon, S., Kung, H.T.: Embedded binarized neural networks. In: EWSN, pp. 168\u2013173 (2017)"},{"issue":"2","key":"8_CR42","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1023\/A:1008643722423","volume":"10","author":"SI Minato","year":"1997","unstructured":"Minato, S.I., Somenzi, F.: Arithmetic Boolean expression manipulator using BDDs. Formal Methods Syst. Des. 10(2), 221\u2013242 (1997). https:\/\/doi.org\/10.1023\/A:1008643722423","journal-title":"Formal Methods Syst. Des."},{"key":"8_CR43","doi-asserted-by":"crossref","unstructured":"Molnar, C., Casalicchio, G., Bischl, B.: Interpretable machine learning - A brief history, state-of-the-art and challenges. CoRR abs\/2010.09337 (2020)","DOI":"10.1007\/978-3-030-65965-3_28"},{"issue":"2","key":"8_CR44","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1016\/j.ic.2005.05.003","volume":"201","author":"A Nakamura","year":"2005","unstructured":"Nakamura, A.: An efficient query learning algorithm for ordered binary decision diagrams. Inf. Comput. 201(2), 178\u2013198 (2005)","journal-title":"Inf. Comput."},{"key":"8_CR45","doi-asserted-by":"crossref","unstructured":"Narodytska, N.: Formal analysis of deep binarized neural networks. In: IJCAI, pp. 5692\u20135696 (2018)","DOI":"10.24963\/ijcai.2018\/811"},{"key":"8_CR46","doi-asserted-by":"crossref","unstructured":"Narodytska, N., Kasiviswanathan, S.P., Ryzhyk, L., Sagiv, M., Walsh, T.: Verifying properties of binarized deep neural networks. In: AAAI, pp. 6615\u20136624 (2018)","DOI":"10.1609\/aaai.v32i1.12206"},{"key":"8_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/978-3-030-24258-9_19","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2019","author":"N Narodytska","year":"2019","unstructured":"Narodytska, N., Shrotri, A., Meel, K.S., Ignatiev, A., Marques-Silva, J.: Assessing heuristic machine learning explanations with model counting. In: Janota, M., Lynce, I. (eds.) SAT 2019. LNCS, vol. 11628, pp. 267\u2013278. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-24258-9_19"},{"key":"8_CR48","unstructured":"Narodytska, N., Zhang, H., Gupta, A., Walsh, T.: In search for a SAT-friendly binarized neural network architecture. In: ICLR (2020)"},{"key":"8_CR49","doi-asserted-by":"crossref","unstructured":"Papernot, N., McDaniel, P.D., Goodfellow, I.J., Jha, S., Celik, Z.B., Swami, A.: Practical black-box attacks against machine learning. In: CCS, pp. 506\u2013519 (2017)","DOI":"10.1145\/3052973.3053009"},{"key":"8_CR50","doi-asserted-by":"crossref","unstructured":"Papernot, N., McDaniel, P.D., Jha, S., Fredrikson, M., Celik, Z.B., Swami, A.: The limitations of deep learning in adversarial settings. In: S&P, pp. 372\u2013387 (2016)","DOI":"10.1109\/EuroSP.2016.36"},{"key":"8_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-642-14295-6_24","volume-title":"Computer Aided Verification","author":"L Pulina","year":"2010","unstructured":"Pulina, L., Tacchella, A.: An abstraction-refinement approach to verification of artificial neural networks. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 243\u2013257. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_24"},{"key":"8_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"525","DOI":"10.1007\/978-3-319-46493-0_32","volume-title":"Computer Vision \u2013 ECCV 2016","author":"M Rastegari","year":"2016","unstructured":"Rastegari, M., Ordonez, V., Redmon, J., Farhadi, A.: XNOR-Net: ImageNet classification using binary convolutional neural networks. In: Leibe, B., Matas, J., Sebe, N., Welling, M. (eds.) ECCV 2016. LNCS, vol. 9908, pp. 525\u2013542. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46493-0_32"},{"key":"8_CR53","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1146\/annurev-bioeng-071516-044442","volume":"19","author":"D Shen","year":"2017","unstructured":"Shen, D., Wu, G., Suk, H.I.: Deep learning in medical image analysis. Annu. Rev. Biomed. Eng. 19, 221\u2013248 (2017)","journal-title":"Annu. Rev. Biomed. Eng."},{"key":"8_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-030-24258-9_25","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2019","author":"A Shih","year":"2019","unstructured":"Shih, A., Darwiche, A., Choi, A.: Verifying binarized neural networks by Angluin-style learning. In: Janota, M., Lynce, I. (eds.) SAT 2019. LNCS, vol. 11628, pp. 354\u2013370. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-24258-9_25"},{"key":"8_CR55","unstructured":"Singh, G., Ganvir, R., P\u00fcschel, M., Vechev, M.T.: Beyond the single neuron convex barrier for neural network certification. In: NeurIPS, pp. 15072\u201315083 (2019)"},{"key":"8_CR56","unstructured":"Singh, G., Gehr, T., Mirman, M., P\u00fcschel, M., Vechev, M.T.: Fast and effective robustness certification. In: NeurIPS, pp. 10825\u201310836 (2018)"},{"key":"8_CR57","doi-asserted-by":"crossref","unstructured":"Singh, G., Gehr, T., P\u00fcschel, M., Vechev, M.T.: An abstract domain for certifying neural networks. Proc. ACM Program. Lang. (POPL) 3, 41:1\u201341:30 (2019)","DOI":"10.1145\/3290354"},{"key":"8_CR58","unstructured":"Somenzi, F.: CUDD: CU decision diagram package (2015)"},{"key":"8_CR59","unstructured":"Szegedy, C., et al.: Intriguing properties of neural networks. In: ICLR (2014)"},{"key":"8_CR60","unstructured":"Tan, M., Le, Q.V.: EfficientNet: rethinking model scaling for convolutional neural networks. In: ICML, pp. 6105\u20136114 (2019)"},{"key":"8_CR61","unstructured":"Tjeng, V., Xiao, K., Tedrake, R.: Evaluating robustness of neural networks with mixed integer programming. In: ICLR (2019)"},{"key":"8_CR62","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/978-3-030-53288-8_2","volume-title":"Computer Aided Verification","author":"H-D Tran","year":"2020","unstructured":"Tran, H.-D., Bak, S., Xiang, W., Johnson, T.T.: Verification of deep convolutional neural networks using ImageStars. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 18\u201342. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_2"},{"key":"8_CR63","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"670","DOI":"10.1007\/978-3-030-30942-8_39","volume-title":"Formal Methods \u2013 The Next 30 Years","author":"H-D Tran","year":"2019","unstructured":"Tran, H.-D., et al.: Star-based reachability analysis of deep neural networks. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 670\u2013686. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30942-8_39"},{"key":"8_CR64","unstructured":"Wan, W., Zhang, Z., Zhu, Y., Zhang, M., Song, F.: Accelerating robustness verification of deep neural networks guided by target labels. CoRR abs\/2007.08520 (2020)"},{"key":"8_CR65","unstructured":"Webb, S., Rainforth, T., Teh, Y.W., Kumar, M.P.: A statistical approach to assessing neural network robustness. In: ICLR (2019)"},{"key":"8_CR66","unstructured":"Weiss, G., Goldberg, Y., Yahav, E.: Extracting automata from recurrent neural networks using queries and counterexamples. In: ICML, pp. 5244\u20135253 (2018)"},{"key":"8_CR67","unstructured":"Wong, E., Kolter, J.Z.: Provable defenses against adversarial examples via the convex outer adversarial polytope. In: ICML, pp. 5283\u20135292 (2018)"},{"issue":"11","key":"8_CR68","first-page":"5777","volume":"29","author":"W Xiang","year":"2018","unstructured":"Xiang, W., Tran, H., Johnson, T.T.: Output reachable set estimation and verification for multilayer neural networks. TNNLS 29(11), 5777\u20135783 (2018)","journal-title":"TNNLS"},{"key":"8_CR69","doi-asserted-by":"crossref","unstructured":"Yang, P., et al.: Improving neural network verification through spurious region guided refinement. CoRR abs\/2010.07722 (2020)","DOI":"10.26226\/morressier.604907f41a80aac83ca25cfb"},{"key":"8_CR70","doi-asserted-by":"crossref","unstructured":"Zhang, Q., Yang, Y., Ma, H., Wu, Y.N.: Interpreting CNNs via decision trees. In: CVPR, pp. 6261\u20136270 (2019)","DOI":"10.1109\/CVPR.2019.00642"},{"key":"8_CR71","doi-asserted-by":"crossref","unstructured":"Zhang, Y., Zhao, Z., Chen, G., Song, F., Chen, T.: BDD4BNN: a BDD-based quantitative analysis framework for binarized neural networks. CoRR abs\/2103.07224 (2021)","DOI":"10.1007\/978-3-030-81685-8_8"}],"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-030-81685-8_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,6]],"date-time":"2023-11-06T04:59:19Z","timestamp":1699246759000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-81685-8_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030816841","9783030816858"],"references-count":71,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-81685-8_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"15 July 2021","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":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"33","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2021\/","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":"290","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":"63","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":"22% - 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":"12","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":"16 tool papers and 5 invited papers are also included.","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)"}}]}}