{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,14]],"date-time":"2026-02-14T03:05:53Z","timestamp":1771038353359,"version":"3.50.1"},"publisher-location":"Cham","reference-count":70,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031377020","type":"print"},{"value":"9783031377037","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,7,18]],"date-time":"2023-07-18T00:00:00Z","timestamp":1689638400000},"content-version":"vor","delay-in-days":198,"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><jats:p>To alleviate the practical constraints for deploying deep neural networks (DNNs) on edge devices, quantization is widely regarded as one promising technique. It reduces the resource requirements for computational power and storage space by quantizing the weights and\/or activation tensors of a DNN into lower bit-width fixed-point numbers, resulting in quantized neural networks (QNNs). While it has been empirically shown to introduce minor accuracy loss, critical verified properties of a DNN might become invalid once quantized. Existing verification methods focus on either individual neural networks (DNNs or QNNs) or quantization error bound for <jats:italic>partial<\/jats:italic> quantization. In this work, we propose a quantization error bound verification method, named , where both weights and activation tensors are quantized.  consists of two parts, i.e., a differential reachability analysis (DRA) and a mixed-integer linear programming (MILP) based verification method. DRA performs difference analysis between the DNN and its quantized counterpart layer-by-layer to compute a tight quantization error interval efficiently. If DRA fails to prove the error bound, then we encode the verification problem into an equivalent MILP problem which can be solved by off-the-shelf solvers. Thus,  is sound, complete, and reasonably efficient. We implement  and conduct extensive experiments, showing its effectiveness and efficiency.\n<\/jats:p>","DOI":"10.1007\/978-3-031-37703-7_20","type":"book-chapter","created":{"date-parts":[[2023,7,17]],"date-time":"2023-07-17T17:02:15Z","timestamp":1689613335000},"page":"413-437","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["QEBVerif: Quantization Error Bound Verification of\u00a0Neural Networks"],"prefix":"10.1007","author":[{"given":"Yedi","family":"Zhang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fu","family":"Song","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jun","family":"Sun","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,7,18]]},"reference":[{"key":"20_CR1","doi-asserted-by":"crossref","unstructured":"Amir, G., Wu, H., Barrett, C.W., Katz, G.: An SMT-based approach for verifying binarized neural networks. In: Proceedings of the 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 203\u2013222 (2021)","DOI":"10.1007\/978-3-030-72013-1_11"},{"key":"20_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: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 731\u2013744 (2019)","DOI":"10.1145\/3314221.3314614"},{"key":"20_CR3","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: Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, pp. 1249\u20131264 (2019)","DOI":"10.1145\/3319535.3354245"},{"issue":"5","key":"20_CR4","doi-asserted-by":"publisher","first-page":"3200","DOI":"10.1109\/TDSC.2021.3088661","volume":"19","author":"L Bu","year":"2022","unstructured":"Bu, L., Zhao, Z., Duan, Y., Song, F.: Taking care of the discretization problem: a comprehensive study of the discretization problem and a black-box adversarial attack in discrete integer domain. IEEE Trans. Dependable Secur. Comput. 19(5), 3200\u20133217 (2022)","journal-title":"IEEE Trans. Dependable Secur. Comput."},{"key":"20_CR5","doi-asserted-by":"crossref","unstructured":"Carlini, N., Wagner, D.A.: Towards evaluating the robustness of neural networks. In: Proceedings of the 2017 IEEE Symposium on Security and Privacy, pp. 39\u201357 (2017)","DOI":"10.1109\/SP.2017.49"},{"key":"20_CR6","doi-asserted-by":"crossref","unstructured":"Chen, G., et al.: Who is real Bob? Adversarial attacks on speaker recognition systems. In: Proceedings of the 42nd IEEE Symposium on Security and Privacy, pp. 694\u2013711 (2021)","DOI":"10.1109\/SP40001.2021.00004"},{"key":"20_CR7","doi-asserted-by":"crossref","unstructured":"Chen, G., Zhao, Z., Song, F., Chen, S., Fan, L., Liu, Y.: AS2T: arbitrary source-to-target adversarial attack on speaker recognition systems. IEEE Trans. Dependable Secur. Comput., 1\u201317 (2022)","DOI":"10.1109\/TDSC.2022.3189397"},{"key":"20_CR8","doi-asserted-by":"crossref","unstructured":"Chen, G., et al.: Towards understanding and mitigating audio adversarial examples for speaker recognition. IEEE Trans. Dependable Secur. Comput., 1\u201317 (2022)","DOI":"10.1109\/TDSC.2022.3220673"},{"key":"20_CR9","unstructured":"Choi, A., Shi, W., Shih, A., Darwiche, A.: Compiling neural networks into tractable Boolean circuits. In: Proceedings of the AAAI Spring Symposium on Verification of Neural Networks (2019)"},{"key":"20_CR10","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: Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"20_CR11","doi-asserted-by":"crossref","unstructured":"Duncan, K., Komendantskaya, E., Stewart, R., Lones, M.: Relative robustness of quantized neural networks against adversarial attacks. In: Proceedings of the International Joint Conference on Neural Networks, pp. 1\u20138 (2020)","DOI":"10.1109\/IJCNN48605.2020.9207596"},{"key":"20_CR12","doi-asserted-by":"crossref","unstructured":"Ehlers, R.: Formal verification of piece-wise linear feed-forward neural networks. In: Proceedings of the 15th International Symposium on Automated Technology for Verification and Analysis, pp. 269\u2013286 (2017)","DOI":"10.1007\/978-3-319-68167-2_19"},{"key":"20_CR13","doi-asserted-by":"crossref","unstructured":"Elboher, Y.Y., Gottschlich, J., Katz, G.: An abstraction-based framework for neural network verification. In: Proceedings of the 32nd International Conference on Computer Aided Verification, pp. 43\u201365 (2020)","DOI":"10.1007\/978-3-030-53288-8_3"},{"key":"20_CR14","doi-asserted-by":"crossref","unstructured":"Eykholt, K., et al.: Robust physical-world attacks on deep learning visual classification. In: Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition, pp. 1625\u20131634 (2018)","DOI":"10.1109\/CVPR.2018.00175"},{"key":"20_CR15","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: Proceedings of the IEEE Symposium on Security and Privacy, pp. 3\u201318 (2018)","DOI":"10.1109\/SP.2018.00058"},{"key":"20_CR16","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":"20_CR17","doi-asserted-by":"crossref","unstructured":"Gong, R., et al.: Differentiable soft quantization: bridging full-precision and low-bit neural networks. In: Proceedings of the IEEE\/CVF International Conference on Computer Vision, pp. 4851\u20134860 (2019)","DOI":"10.1109\/ICCV.2019.00495"},{"key":"20_CR18","unstructured":"Google: Tensorflow lite (2022). https:\/\/www.tensorflow.org\/lite"},{"key":"20_CR19","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: Proceedings of the 32nd IEEE International Symposium on Software Reliability Engineering, pp. 345\u2013356 (2021)","DOI":"10.1109\/ISSRE52982.2021.00044"},{"key":"20_CR20","unstructured":"Gurobi: a most powerful mathematical optimization solver (2018). https:\/\/www.gurobi.com\/"},{"key":"20_CR21","unstructured":"Han, S., Mao, H., Dally, W.J.: Deep compression: compressing deep neural network with pruning, trained quantization and Huffman coding. In: Proceedings of the 4th International Conference on Learning Representations (2016)"},{"key":"20_CR22","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Lechner, M., Zikelic, D.: Scalable verification of quantized neural networks. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol. 35, pp. 3787\u20133795 (2021)","DOI":"10.1609\/aaai.v35i5.16496"},{"issue":"6","key":"20_CR23","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_CR24","doi-asserted-by":"crossref","unstructured":"Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety verification of deep neural networks. In: Proceedings of the 29th International Conference on Computer Aided Verification, pp. 3\u201329 (2017)","DOI":"10.1007\/978-3-319-63387-9_1"},{"key":"20_CR25","doi-asserted-by":"crossref","unstructured":"Jacob, B., et al.: Quantization and training of neural networks for efficient integer-arithmetic-only inference. In: Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition, pp. 2704\u20132713 (2018)","DOI":"10.1109\/CVPR.2018.00286"},{"issue":"3","key":"20_CR26","doi-asserted-by":"publisher","first-page":"598","DOI":"10.2514\/1.G003724","volume":"42","author":"KD Julian","year":"2019","unstructured":"Julian, K.D., Kochenderfer, M.J., Owen, M.P.: Deep neural network compression for aircraft collision avoidance systems. J. Guid. Control. Dyn. 42(3), 598\u2013608 (2019)","journal-title":"J. Guid. Control. Dyn."},{"key":"20_CR27","doi-asserted-by":"crossref","unstructured":"Jung, S., et al.: Learning to quantize deep networks by optimizing quantization intervals with task loss. In: Proceedings of the IEEE\/CVF Conference on Computer Vision and Pattern Recognition, pp. 4350\u20134359 (2019)","DOI":"10.1109\/CVPR.2019.00448"},{"key":"20_CR28","doi-asserted-by":"crossref","unstructured":"Karpathy, A., Toderici, G., Shetty, S., Leung, T., Sukthankar, R., Li, F.: Large-scale video classification with convolutional neural networks. In: Proceedings of 2014 IEEE Conference on Computer Vision and Pattern Recognition, pp. 1725\u20131732 (2014)","DOI":"10.1109\/CVPR.2014.223"},{"key":"20_CR29","doi-asserted-by":"crossref","unstructured":"Katz, G., Barrett, C.W., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: an efficient SMT solver for verifying deep neural networks. In: Proceedings of the 29th International Conference on Computer Aided Verification, pp. 97\u2013117 (2017)","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"20_CR30","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, pp. 443\u2013452 (2019)","DOI":"10.1007\/978-3-030-25540-4_26"},{"key":"20_CR31","unstructured":"LeCun, Y., Cortes, C.: MNIST handwritten digit database (2010)"},{"key":"20_CR32","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":"20_CR33","unstructured":"Li, J., Drummond, R., Duncan, S.R.: Robust error bounds for quantised and pruned neural networks. In: Proceedings of the 3rd Annual Conference on Learning for Dynamics and Control, pp. 361\u2013372 (2021)"},{"key":"20_CR34","doi-asserted-by":"crossref","unstructured":"Li, R., et al.: Prodeep: a platform for robustness verification of deep neural networks. In: Proceedings of the 28th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pp. 1630\u20131634 (2020)","DOI":"10.1145\/3368089.3417918"},{"key":"20_CR35","unstructured":"Lin, D.D., Talathi, S.S., Annapureddy, V.S.: Fixed point quantization of deep convolutional networks. In: Proceedings of the 33nd International Conference on Machine Learning, pp. 2849\u20132858 (2016)"},{"key":"20_CR36","unstructured":"Lin, J., Gan, C., Han, S.: Defensive quantization: when efficiency meets robustness. In: Proceedings of the International Conference on Learning Representations (2019)"},{"key":"20_CR37","unstructured":"Liu, J., Xing, Y., Shi, X., Song, F., Xu, Z., Ming, Z.: Abstraction and refinement: towards scalable and exact verification of neural networks. CoRR abs\/2207.00759 (2022)"},{"issue":"6","key":"20_CR38","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":"20_CR39","unstructured":"Lomuscio, A., Maganti, L.: An approach to reachability analysis for feed-forward ReLU neural networks. CoRR abs\/1706.07351 (2017)"},{"key":"20_CR40","doi-asserted-by":"crossref","unstructured":"Mistry, S., Saha, I., Biswas, S.: An MILP encoding for efficient verification of quantized deep neural networks. IEEE Trans. Comput.-Aided Des. Integrated Circuits Syst. (Early Access) (2022)","DOI":"10.1109\/TCAD.2022.3197697"},{"key":"20_CR41","doi-asserted-by":"crossref","unstructured":"Mohammadinejad, S., Paulsen, B., Deshmukh, J.V., Wang, C.: DiffRNN: differential verification of recurrent neural networks. In: Proceedings of the 19th International Conference on Formal Modeling and Analysis of Timed Systems, pp. 117\u2013134 (2021)","DOI":"10.1007\/978-3-030-85037-1_8"},{"key":"20_CR42","doi-asserted-by":"crossref","unstructured":"Moore, R.E., Kearfott, R.B., Cloud, M.J.: Introduction to Interval Analysis, vol. 110. SIAM (2009)","DOI":"10.1137\/1.9780898717716"},{"key":"20_CR43","unstructured":"Nagel, M., Amjad, R.A., Van Baalen, M., Louizos, C., Blankevoort, T.: Up or down? Adaptive rounding for post-training quantization. In: Proceedings of the International Conference on Machine Learning, pp. 7197\u20137206 (2020)"},{"key":"20_CR44","unstructured":"Nagel, M., Fournarakis, M., Amjad, R.A., Bondarenko, Y., van Baalen, M., Blankevoort, T.: A white paper on neural network quantization. arXiv preprint arXiv:2106.08295 (2021)"},{"issue":"2","key":"20_CR45","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":"20_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: Proceedings of the AAAI Conference on Artificial Intelligence, pp. 6615\u20136624 (2018)","DOI":"10.1609\/aaai.v32i1.12206"},{"key":"20_CR47","unstructured":"Odena, A., Olsson, C., Andersen, D.G., Goodfellow, I.J.: TensorFuzz: debugging neural networks with coverage-guided fuzzing. In: Proceedings of the 36th International Conference on Machine Learning, pp. 4901\u20134911 (2019)"},{"key":"20_CR48","doi-asserted-by":"crossref","unstructured":"Paulsen, B., Wang, J., Wang, C.: ReluDiff: differential verification of deep neural networks. In: 2020 IEEE\/ACM 42nd International Conference on Software Engineering (ICSE), pp. 714\u2013726. IEEE (2020)","DOI":"10.1145\/3377811.3380337"},{"key":"20_CR49","doi-asserted-by":"crossref","unstructured":"Paulsen, B., Wang, J., Wang, J., Wang, C.: NeuroDiff: scalable differential verification of neural networks using fine-grained approximation. In: Proceedings of the 35th IEEE\/ACM International Conference on Automated Software Engineering, pp. 784\u2013796 (2020)","DOI":"10.1145\/3324884.3416560"},{"key":"20_CR50","doi-asserted-by":"crossref","unstructured":"Pei, K., Cao, Y., Yang, J., Jana, S.: DeepXplore: automated whitebox testing of deep learning systems. In: Proceedings of the 26th Symposium on Operating Systems Principles, pp. 1\u201318 (2017)","DOI":"10.1145\/3132747.3132785"},{"key":"20_CR51","doi-asserted-by":"crossref","unstructured":"Pulina, L., Tacchella, A.: An abstraction-refinement approach to verification of artificial neural networks. In: Proceedings of the 22nd International Conference on Computer Aided Verification, pp. 243\u2013257 (2010)","DOI":"10.1007\/978-3-642-14295-6_24"},{"key":"20_CR52","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":"20_CR53","doi-asserted-by":"crossref","unstructured":"Shih, A., Darwiche, A., Choi, A.: Verifying binarized neural networks by local automaton learning. In: Proceedings of the AAAI Spring Symposium on Verification of Neural Networks (2019)","DOI":"10.1007\/978-3-030-24258-9_25"},{"key":"20_CR54","unstructured":"Singh, G., Ganvir, R., P\u00fcschel, M., Vechev, M.T.: Beyond the single neuron convex barrier for neural network certification. In: Proceedings of the Annual Conference on Neural Information Processing Systems, pp. 15072\u201315083 (2019)"},{"key":"20_CR55","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"},{"issue":"9","key":"20_CR56","doi-asserted-by":"publisher","first-page":"5210","DOI":"10.1002\/int.22510","volume":"36","author":"F Song","year":"2021","unstructured":"Song, F., Lei, Y., Chen, S., Fan, L., Liu, Y.: Advanced evasion attacks and mitigations on practical ml-based phishing website classifiers. Int. J. Intell. Syst. 36(9), 5210\u20135240 (2021)","journal-title":"Int. J. Intell. Syst."},{"key":"20_CR57","doi-asserted-by":"crossref","unstructured":"Tian, Y., Pei, K., Jana, S., Ray, B.: DeepTest: automated testing of deep-neural-network-driven autonomous cars. In: Proceedings of the 40th International Conference on Software Engineering, pp. 303\u2013314 (2018)","DOI":"10.1145\/3180155.3180220"},{"key":"20_CR58","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":"20_CR59","doi-asserted-by":"crossref","unstructured":"Tran, H., et al.: Star-based reachability analysis of deep neural networks. In: Proceedings of the 3rd World Congress on Formal Methods, pp. 670\u2013686 (2019)","DOI":"10.1007\/978-3-030-30942-8_39"},{"key":"20_CR60","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, pp. 1599\u20131614 (2018)"},{"key":"20_CR61","unstructured":"WikiChip: FSD chip - tesla. https:\/\/en.wikichip.org\/wiki\/tesla_(car_company)\/fsd_chip. Accessed 30 Apr 2022"},{"key":"20_CR62","doi-asserted-by":"crossref","unstructured":"Yang, P., et al.: Improving neural network verification through spurious region guided refinement. In: Groote, J.F., Larsen, K.G. (eds.) Proceedings of 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 389\u2013408 (2021)","DOI":"10.26226\/morressier.604907f41a80aac83ca25cfb"},{"issue":"2","key":"20_CR63","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1109\/TSE.2019.2962027","volume":"48","author":"JM Zhang","year":"2022","unstructured":"Zhang, J.M., Harman, M., Ma, L., Liu, Y.: Machine learning testing: survey, landscapes and horizons. IEEE Trans. Software Eng. 48(2), 1\u201336 (2022)","journal-title":"IEEE Trans. Software Eng."},{"key":"20_CR64","unstructured":"Zhang, Y., Song, F., Sun, J.: QEBVerif (2023). https:\/\/github.com\/S3L-official\/QEBVerif"},{"key":"20_CR65","doi-asserted-by":"crossref","unstructured":"Zhang, Y., Song, F., Sun, J.: QEBVerif: quantization error bound verification of neural networks. CoRR abs\/2212.02781 (2023)","DOI":"10.1007\/978-3-031-37703-7_20"},{"key":"20_CR66","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-030-81685-8_8","volume-title":"Computer Aided Verification","author":"Y Zhang","year":"2021","unstructured":"Zhang, Y., Zhao, Z., Chen, G., Song, F., Chen, T.: BDD4BNN: a BDD-based quantitative analysis framework for binarized neural networks. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 175\u2013200. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_8"},{"key":"20_CR67","doi-asserted-by":"crossref","unstructured":"Zhang, Y., Zhao, Z., Chen, G., Song, F., Chen, T.: Precise quantitative analysis of binarized neural networks: a BDD-based approach. ACM Trans. Software Eng. Methodol. 32(3) (2023)","DOI":"10.1145\/3563212"},{"key":"20_CR68","doi-asserted-by":"crossref","unstructured":"Zhang, Y., et al.: QVIP: an ILP-based formal verification approach for quantized neural networks. In: Proceedings of the 37th IEEE\/ACM International Conference on Automated Software Engineering, pp. 82:1\u201382:13 (2023)","DOI":"10.1145\/3551349.3556916"},{"key":"20_CR69","doi-asserted-by":"crossref","unstructured":"Zhao, Z., Chen, G., Wang, J., Yang, Y., Song, F., Sun, J.: Attack as defense: characterizing adversarial examples using robustness. In: Proceedings of the 30th ACM SIGSOFT International Symposium on Software Testing and Analysis, pp. 42\u201355 (2021)","DOI":"10.1145\/3460319.3464822"},{"key":"20_CR70","doi-asserted-by":"publisher","unstructured":"Zhao, Z., Zhang, Y., Chen, G., Song, F., Chen, T., Liu, J.: CLEVEREST: accelerating CEGAR-based neural network verification via adversarial attacks. In: Singh, G., Urban, C. (eds.) Proceedings of the 29th International Symposium on Static Analysis, pp. 449\u2013473 (2022). https:\/\/doi.org\/10.1007\/978-3-031-22308-2_20","DOI":"10.1007\/978-3-031-22308-2_20"}],"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-031-37703-7_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,26]],"date-time":"2023-08-26T11:02:17Z","timestamp":1693047737000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-37703-7_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031377020","9783031377037"],"references-count":70,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-37703-7_20","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":"18 July 2023","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":"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":"17 July 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 July 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"35","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.i-cav.org\/2023\/","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":"hotcrp","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"261","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":"67","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","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":"11","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)"}}]}}