{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,3]],"date-time":"2026-09-03T15:16:16Z","timestamp":1788448576762,"version":"build-2803163510"},"reference-count":90,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T00:00:00Z","timestamp":1744156800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"name":"Strategic Priority Research Program of Chinese Academy of Sciences","award":["XDA0320101"],"award-info":[{"award-number":["XDA0320101"]}]},{"name":"Ministry of Education, Singapore under its Academic Research Fund Tier 2","award":["T2EP20222-0037"],"award-info":[{"award-number":["T2EP20222-0037"]}]},{"name":"Ministry of Education, Singapore under its Academic Research Fund Tier 3","award":["MOET32020-0003"],"award-info":[{"award-number":["MOET32020-0003"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,4,9]]},"abstract":"<jats:p>In the rapidly evolving landscape of neural network security, the resilience of neural networks against bit-flip attacks (i.e., an attacker maliciously flips an extremely small amount of bits within its parameter storage memory system to induce harmful behavior), has emerged as a relevant area of research. Existing studies suggest that quantization may serve as a viable defense against such attacks. Recognizing the documented susceptibility of real-valued neural networks to such attacks and the comparative robustness of quantized neural networks (QNNs), in this work, we introduce BFAVerifier, the first verification framework designed to formally verify the absence of bit-flip attacks against QNNs or to identify all vulnerable parameters in a sound and rigorous manner. BFAVerifier comprises two integral components: an abstraction-based method and an MILP-based method. Specifically, we first conduct a reachability analysis with respect to symbolic parameters that represent the potential bit-flip attacks, based on a novel abstract domain with a sound guarantee. If the reachability analysis fails to prove the resilience of such attacks, then we encode this verification problem into an equivalent MILP problem which can be solved by off-the-shelf solvers. Therefore, BFAVerifier is sound, complete, and reasonably efficient. We conduct extensive experiments, which demonstrate its effectiveness and efficiency across various activation functions, quantization bit-widths, and adversary capabilities.<\/jats:p>","DOI":"10.1145\/3720471","type":"journal-article","created":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T13:48:26Z","timestamp":1744206506000},"page":"984-1014","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Verification of Bit-Flip Attacks against Quantized Neural Networks"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1005-2114","authenticated-orcid":false,"given":"Yedi","family":"Zhang","sequence":"first","affiliation":[{"name":"National University of Singapore, Singapore, Singapore"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-6412-2149","authenticated-orcid":false,"given":"Lei","family":"Huang","sequence":"additional","affiliation":[{"name":"ShanghaiTech University, Shanghai, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3800-2565","authenticated-orcid":false,"given":"Pengfei","family":"Gao","sequence":"additional","affiliation":[{"name":"ByteDance Inc, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0581-2679","authenticated-orcid":false,"given":"Fu","family":"Song","sequence":"additional","affiliation":[{"name":"Institute of Software at Chinese Academy of Sciences, Key Laboratory of System Software (Chinese Academy of Sciences) and State Key Laboratory of Computer Science, Beijing, China"},{"name":"University of Chinese Academy of Sciences, Beijing, China"},{"name":"Nanjing Institute of Software Technology, Nanjing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3545-1392","authenticated-orcid":false,"given":"Jun","family":"Sun","sequence":"additional","affiliation":[{"name":"Singapore Management University, Singapore, Singapore"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6512-8326","authenticated-orcid":false,"given":"Jin Song","family":"Dong","sequence":"additional","affiliation":[{"name":"National University of Singapore, Singapore, Singapore"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","unstructured":"2019. IEEE Standard for Floating-Point Arithmetic. IEEE Std 754-2019 (Revision of IEEE 754-2008) (2019) 1\u201384. https:\/\/doi.org\/10.1109\/IEEESTD.2019.8766229 10.1109\/IEEESTD.2019.8766229","DOI":"10.1109\/IEEESTD.2019.8766229"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","unstructured":"Pranav Ashok Vahid Hashemi Jan Kret\u00ednsk\u00fd and Stefanie Mohr. 2020. DeepAbstract: Neural Network Abstraction for Accelerating Verification. In Proceedings of the 18th International Symposium on Automated Technology for Verification and Analysis. 92\u2013107. https:\/\/doi.org\/10.1007\/978-3-030-59152-6_5 10.1007\/978-3-030-59152-6_5","DOI":"10.1007\/978-3-030-59152-6_5"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2012.2188769"},{"key":"e_1_3_1_5_2","unstructured":"BFAVerifier. 2025. https:\/\/github.com\/zhangyedi\/BFAVerifier."},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","unstructured":"Eli Biham and Adi Shamir. 1997. Differential Fault Analysis of Secret Key Cryptosystems. In Proceedings of the 17th Annual International Cryptology Conference. 513\u2013525. https:\/\/doi.org\/10.1007\/BFB0052259 10.1007\/BFB0052259","DOI":"10.1007\/BFB0052259"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","unstructured":"Dan Boneh Richard A. DeMillo and Richard J. Lipton. 1997. On the Importance of Checking Cryptographic Protocols for Faults (Extended Abstract). In Proceeding of the International Conference on the Theory and Application of Cryptographic Techniques. 37\u201351. https:\/\/doi.org\/10.1007\/3-540-69053-0_4 10.1007\/3-540-69053-0_4","DOI":"10.1007\/3-540-69053-0_4"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3278519"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1109\/TDSC.2021.3088661"},{"key":"e_1_3_1_10_2","unstructured":"Rudy Bunel Ilker Turkaslan Philip H. S. Torr Pushmeet Kohli and Pawan Kumar Mudigonda. 2018. A Unified View of Piecewise Linear Neural Network Verification. In Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018 NeurIPS 2018 December 3-8 2018 Montr\u00e9al Canada. 4795\u20134804. https:\/\/proceedings.neurips.cc\/paper\/2018\/hash\/be53d253d6bc3258a8160556dda3e9b2-Abstract.html"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","unstructured":"Guangke Chen Sen Chen Lingling Fan Xiaoning Du Zhe Zhao Fu Song and Yang Liu. 2021. Who is Real Bob? Adversarial Attacks on Speaker Recognition Systems. In Proceedings of the 42nd IEEE Symposium on Security and Privacy. https:\/\/doi.org\/10.1109\/SP40001.2021.00004 10.1109\/SP40001.2021.00004","DOI":"10.1109\/SP40001.2021.00004"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2024.241323"},{"key":"e_1_3_1_13_2","first-page":"2437","volume-title":"32nd USENIX Security Symposium, USENIX Security 2023, Anaheim, CA, USA, August 9-11, 2023","author":"Chen Guangke","year":"2023","unstructured":"Guangke Chen, Yedi Zhang, Zhe Zhao, and Fu Song. 2023. QFA2SR: Query-Free Adversarial Transfer Attacks to Speaker Recognition Systems. In 32nd USENIX Security Symposium, USENIX Security 2023, Anaheim, CA, USA, August 9-11, 2023, Joseph A. Calandrino and Carmela Troncoso (Eds.). USENIX Association, 2437\u20132454. https:\/\/www.usenix.org\/conference\/usenixsecurity23\/presentation\/chen-guangke"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","unstructured":"Chih-Hong Cheng Georg N\u00fchrenberg and Harald Ruess. 2017. Maximum Resilience of Artificial Neural Networks. In Proceedings of the 15th International Symposium on Automated Technology for Verification and Analysis (ATVA). 251\u2013268. https:\/\/doi.org\/10.1007\/978-3-319-68167-2_18 10.1007\/978-3-319-68167-2_18","DOI":"10.1007\/978-3-319-68167-2_18"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00089"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2023.24337"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","unstructured":"Jianshuo Dong Han Qiu Yiming Li Tianwei Zhang Yuanjie Li Zeqi Lai Chao Zhang and Shu-Tao Xia. 2023. One-bit Flip is All You Need: When Bit-flip Attack Meets Model Training. In IEEE\/CVF International Conference on Computer Vision ICCV 2023 Paris France October 1-6 2023. IEEE 4665\u20134675. https:\/\/doi.org\/10.1109\/ICCV51070.2023.00432 10.1109\/ICCV51070.2023.00432","DOI":"10.1109\/ICCV51070.2023.00432"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","unstructured":"Shi Dong Ping Wang and Khushnood Abbas. 2021. A survey on deep learning and its applications. Comput. Sci. Rev. 40 (2021) 100379. https:\/\/doi.org\/10.1016\/J.COSREV.2021.100379 10.1016\/J.COSREV.2021.100379","DOI":"10.1016\/J.COSREV.2021.100379"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","unstructured":"Mathieu Dumont Pierre-Alain Mo\u00ebllic Raphael Viera Jean-Max Dutertre and R\u00e9mi Bernhard. 2021. An Overview of Laser Injection against Embedded Neural Network Models. In 2021 IEEE 7th World Forum on Internet of Things (WF-IoT). 616\u2013621. https:\/\/doi.org\/10.1109\/WF-IoT51360.2021.9595075 10.1109\/WF-IoT51360.2021.9595075","DOI":"10.1109\/WF-IoT51360.2021.9595075"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","unstructured":"Yizhak Yisrael Elboher Justin Gottschlich and Guy Katz. 2020. An Abstraction-Based Framework for Neural Network Verification. In Proceedings of the 32nd International Conference on Computer Aided Verification. 43\u201365. https:\/\/doi.org\/10.1007\/978-3-030-53288-8_3 10.1007\/978-3-030-53288-8_3","DOI":"10.1007\/978-3-030-53288-8_3"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/S10601-018-9285-6"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","unstructured":"Timon Gehr Matthew Mirman Dana Drachsler-Cohen Petar Tsankov Swarat Chaudhuri and Martin T. Vechev. 2018. AI2: Safety and Robustness Certification of Neural Networks with Abstract Interpretation. In Proceedings of the 2018 IEEE Symposium on Security and Privacy. 3\u201318. https:\/\/doi.org\/10.1109\/SP.2018.00058 10.1109\/SP.2018.00058","DOI":"10.1109\/SP.2018.00058"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","unstructured":"Amir Gholami Sehoon Kim Zhen Dong Zhewei Yao Michael W. Mahoney and Kurt Keutzer. 2021. A Survey of Quantization Methods for Efficient Neural Network Inference. CoRR abs\/2103.13630 (2021). https:\/\/doi.org\/10.48550\/arXiv.2103.13630 10.48550\/arXiv.2103.13630 arXiv:2103.13630","DOI":"10.48550\/arXiv.2103.13630"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","unstructured":"Mirco Giacobbe Thomas A. Henzinger and Mathias Lechner. 2020. How Many Bits Does it Take to Quantize Your Neural Network?. In Proceedings of the 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). 79\u201397. https:\/\/doi.org\/10.1007\/978-3-030-45237-7_5 10.1007\/978-3-030-45237-7_5","DOI":"10.1007\/978-3-030-45237-7_5"},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","unstructured":"Ruihao Gong Xianglong Liu Shenghu Jiang Tianxiang Li Peng Hu Jiazhen Lin Fengwei Yu and Junjie Yan. 2019. Differentiable Soft Quantization: Bridging Full-Precision and Low-Bit Neural Networks. In Proceedings of the IEEE\/CVF International Conference on Computer Vision (ICCV). 4851\u20134860. https:\/\/doi.org\/10.1109\/ICCV.2019.00495 10.1109\/ICCV.2019.00495","DOI":"10.1109\/ICCV.2019.00495"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","unstructured":"Xingwu Guo Wenjie Wan Zhaodi Zhang Min Zhang Fu Song and Xuejun Wen. 2021. Eager Falsification for Accelerating Robustness Verification of Deep Neural Networks. In Proceedings of the 32nd IEEE International Symposium on Software Reliability Engineering. 345\u2013356. https:\/\/doi.org\/10.1109\/ISSRE52982.2021.00044 10.1109\/ISSRE52982.2021.00044","DOI":"10.1109\/ISSRE52982.2021.00044"},{"key":"e_1_3_1_27_2","unstructured":"Gurobi. 2018. A most powerful mathematical optimization solver. https:\/\/www.gurobi.com\/."},{"key":"e_1_3_1_28_2","unstructured":"Song Han Huizi Mao and William J. Dally. 2016. Deep Compression: Compressing Deep Neural Network with Pruning Trained Quantization and Huffman Coding. In 4th International Conference on Learning Representations ICLR 2016 San Juan Puerto Rico May 2-4 2016 Conference Track Proceedings Yoshua Bengio and Yann LeCun (Eds.). http:\/\/arxiv.org\/abs\/1510.00149"},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","unstructured":"Zhezhi He Adnan Siraj Rakin Jingtao Li Chaitali Chakrabarti and Deliang Fan. 2020. Defending and harnessing the bit-flip based adversarial weight attack. In Proceedings of the IEEE\/CVF Conference on Computer Vision and Pattern Recognition. 14095\u201314103. https:\/\/doi.org\/10.1109\/CVPR42600.2020.01410 10.1109\/CVPR42600.2020.01410","DOI":"10.1109\/CVPR42600.2020.01410"},{"key":"e_1_3_1_30_2","doi-asserted-by":"publisher","unstructured":"Thomas A. Henzinger Mathias Lechner and Dorde Zikelic. 2021. Scalable Verification of Quantized Neural Networks. In Proceedings of the 35th AAAI Conference on Artificial Intelligence (AAAI). 3787\u20133795. https:\/\/doi.org\/10.1609\/AAAI.V35I5.16496 10.1609\/AAAI.V35I5.16496","DOI":"10.1609\/AAAI.V35I5.16496"},{"key":"e_1_3_1_31_2","first-page":"497","volume-title":"28th USENIX Security Symposium, USENIX Security 2019, Santa Clara, CA, USA, August 14-16, 2019","author":"Hong Sanghyun","year":"2019","unstructured":"Sanghyun Hong, Pietro Frigo, Yigitcan Kaya, Cristiano Giuffrida, and Tudor Dumitras. 2019. Terminal Brain Damage: Exposing the Graceless Degradation in Deep Neural Networks Under Hardware Fault Attacks. In 28th USENIX Security Symposium, USENIX Security 2019, Santa Clara, CA, USA, August 14-16, 2019, Nadia Heninger and Patrick Traynor (Eds.). USENIX Association, 497\u2013514. https:\/\/www.usenix.org\/conference\/usenixsecurity19\/presentation\/hong"},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","DOI":"10.1609\/AAAI.V38I19.30108"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","unstructured":"Benoit Jacob Skirmantas Kligys Bo Chen Menglong Zhu Matthew Tang Andrew G. Howard Hartwig Adam and Dmitry Kalenichenko. 2018. Quantization and Training of Neural Networks for Efficient Integer-Arithmetic-Only Inference. In Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition (CVPR). 2704\u20132713. https:\/\/doi.org\/10.1109\/CVPR.2018.00286 10.1109\/CVPR.2018.00286","DOI":"10.1109\/CVPR.2018.00286"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.2514\/1.G003724"},{"key":"e_1_3_1_35_2","doi-asserted-by":"publisher","unstructured":"Guy Katz Clark W. Barrett David L. Dill Kyle Julian and Mykel J. Kochenderfer. 2017. Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. In Proceedings of the 29th International Conference on Computer Aided Verification. 97\u2013117. https:\/\/doi.org\/10.1007\/978-3-319-63387-9_5 10.1007\/978-3-319-63387-9_5","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"e_1_3_1_36_2","doi-asserted-by":"publisher","unstructured":"Guy Katz Derek A. Huang Duligur Ibeling Kyle Julian Christopher Lazarus Rachel Lim Parth Shah Shantanu Thakoor Haoze Wu Aleksandar Zeljic David L. Dill Mykel J. Kochenderfer and Clark W. Barrett. 2019. The Marabou Framework for Verification and Analysis of Deep Neural Networks. In Proceedings of the 31st International Conference on Computer Aided Verification. 443\u2013452. https:\/\/doi.org\/10.1007\/978-3-030-25540-4_26 10.1007\/978-3-030-25540-4_26","DOI":"10.1007\/978-3-030-25540-4_26"},{"key":"e_1_3_1_37_2","unstructured":"Faiq Khalid Muhammad Abdullah Hanif and Muhammad Shafique. 2021. Exploiting Vulnerabilities in Deep Neural Networks: Adversarial and Fault-Injection Attacks. CoRR abs\/2105.03251 (2021). arXiv:2105.03251 https:\/\/arxiv.org\/abs\/2105.03251"},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.MICPRO.2022.104710"},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","DOI":"10.1109\/ISCA.2014.6853210"},{"key":"e_1_3_1_40_2","unstructured":"Yann LeCun and Corinna Cortes. 2010. MNIST handwritten digit database."},{"key":"e_1_3_1_41_2","doi-asserted-by":"publisher","unstructured":"Kyungmi Lee and Anantha P. Chandrakasan. 2022. SparseBFA: Attacking Sparse Deep Neural Networks with the Worst-Case Bit Flips on Coordinates. In ICASSP 2022 - 2022 IEEE International Conference on Acoustics Speech and Signal Processing (ICASSP). 4208\u20134212. https:\/\/doi.org\/10.1109\/ICASSP43922.2022.9747337 10.1109\/ICASSP43922.2022.9747337","DOI":"10.1109\/ICASSP43922.2022.9747337"},{"key":"e_1_3_1_42_2","doi-asserted-by":"publisher","unstructured":"Jianlin Li Jiangchao Liu Pengfei Yang Liqian Chen Xiaowei Huang and Lijun Zhang. 2019. Analyzing Deep Neural Networks with Symbolic Propagation: Towards Higher Precision and Faster Verification. In Proceedings of the 26th International Symposium on Static Analysis. 296\u2013319. https:\/\/doi.org\/10.1007\/978-3-030-32304-2_15 10.1007\/978-3-030-32304-2_15","DOI":"10.1007\/978-3-030-32304-2_15"},{"key":"e_1_3_1_43_2","doi-asserted-by":"publisher","unstructured":"Qun Li Yuan Meng Chen Tang Jiacheng Jiang and Zhi Wang. 2024. Investigating the Impact of Quantization on Adversarial Robustness. CoRR abs\/2404.05639 (2024). https:\/\/doi.org\/10.48550\/arxiv.2404.05639 10.48550\/arxiv.2404.05639 arXiv:2404.05639","DOI":"10.48550\/arxiv.2404.05639"},{"key":"e_1_3_1_44_2","doi-asserted-by":"publisher","unstructured":"Renjue Li Jianlin Li Cheng-Chao Huang Pengfei Yang Xiaowei Huang Lijun Zhang Bai Xue and Holger Hermanns. 2020. 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. 1630\u20131634. https:\/\/doi.org\/10.1145\/3368089.3417918 10.1145\/3368089.3417918","DOI":"10.1145\/3368089.3417918"},{"key":"e_1_3_1_45_2","volume-title":"33rd USENIX Security Symposium, USENIX Security 2024, Philadelphia, PA, USA, August 14-16, 2024","author":"Li Shaofeng","year":"2024","unstructured":"Shaofeng Li, Xinyu Wang, Minhui Xue, Haojin Zhu, Zhi Zhang, Yansong Gao, Wen Wu, and Xuemin (Sherman) Shen. 2024. Yes, One-Bit-Flip Matters! Universal DNN Model Inference Depletion with Runtime Code Fault Injection. In 33rd USENIX Security Symposium, USENIX Security 2024, Philadelphia, PA, USA, August 14-16, 2024, Davide Balzarotti and Wenyuan Xu (Eds.). USENIX Association. https:\/\/www.usenix.org\/conference\/usenixsecurity24\/presentation\/li-shaofeng"},{"key":"e_1_3_1_46_2","doi-asserted-by":"publisher","DOI":"10.1145\/3644387"},{"key":"e_1_3_1_47_2","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2022.3211411"},{"key":"e_1_3_1_48_2","doi-asserted-by":"publisher","DOI":"10.1109\/DAC18072.2020.9218577"},{"key":"e_1_3_1_49_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2017.8203770"},{"key":"e_1_3_1_50_2","unstructured":"Alessio Lomuscio and Lalit Maganti. 2017. An approach to reachability analysis for feed-forward ReLU neural networks. CoRR abs\/1706.07351 (2017). arXiv:1706.07351 http:\/\/arxiv.org\/abs\/1706.07351"},{"key":"e_1_3_1_51_2","unstructured":"muellch Gleb Makarchuk GgnDp skcho Gagandeep Singh Fran\u00e7ois Serre Tobias Zimmermann Anian Ruoss Mark M\u00fcller Shachar Itzhaky Jingxuan He Haoze(Andrew) Wu Isac Andrei jorgenavas Jose Calderon and Jianlin Li. 2023. eth-sri\/ELINA. https:\/\/github.com\/eth-sri\/ELINA"},{"key":"e_1_3_1_52_2","volume-title":"Proceedings of the Fourth Conference on Machine Learning and Systems, MLSys 2021, virtual, April 5-9, 2021","author":"M\u00fcller Christoph","year":"2021","unstructured":"Christoph M\u00fcller, Fran\u00e7ois Serre, Gagandeep Singh, Markus P\u00fcschel, and Martin T. Vechev. 2021. Scaling Polyhedral Neural Network Verification on GPUs. In Proceedings of the Fourth Conference on Machine Learning and Systems, MLSys 2021, virtual, April 5-9, 2021, Alex Smola, Alex Dimakis, and Ion Stoica (Eds.). mlsys.org. https:\/\/proceedings.mlsys.org\/paper_files\/paper\/2021\/hash\/7c98f9c7ab2df90911da23f9ce72ed6e-Abstract.html"},{"key":"e_1_3_1_53_2","doi-asserted-by":"publisher","DOI":"10.3390\/FI15060199"},{"key":"e_1_3_1_54_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2019.2915318"},{"key":"e_1_3_1_55_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-19992-9_25"},{"key":"e_1_3_1_56_2","doi-asserted-by":"publisher","unstructured":"Long H Pham and Jun Sun. 2022. Verifying Neural Networks Against Backdoor Attacks. In Proceedings of the 34th International Conference on Computer Aided Verification (CAV). 171\u2013192. https:\/\/doi.org\/10.1007\/978-3-031-13185-1_9 10.1007\/978-3-031-13185-1_9","DOI":"10.1007\/978-3-031-13185-1_9"},{"key":"e_1_3_1_57_2","doi-asserted-by":"publisher","DOI":"10.1145\/3650212.3680322"},{"key":"e_1_3_1_58_2","unstructured":"Pavithra Prabhakar and Zahra Rahimi Afzal. 2019. Abstraction based Output Range Analysis for Neural Networks. In Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019 NeurIPS 2019 December 8-14 2019 Vancouver BC Canada Hanna M. Wallach Hugo Larochelle Alina Beygelzimer Florence d\u2019Alch\u00e9-Buc Emily B. Fox and Roman Garnett (Eds.). 15762\u201315772. https:\/\/proceedings.neurips.cc\/paper\/2019\/hash\/5df0385cba256a135be596dbe28fa7aa-Abstract.html"},{"key":"e_1_3_1_59_2","doi-asserted-by":"publisher","DOI":"10.3390\/electronics12040853"},{"key":"e_1_3_1_60_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP46214.2022.9833743"},{"key":"e_1_3_1_61_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICCV.2019.00130"},{"key":"e_1_3_1_62_2","first-page":"1919","volume-title":"30th USENIX Security Symposium (USENIX Security 21)","author":"Rakin Adnan Siraj","year":"2021","unstructured":"Adnan Siraj Rakin, Yukui Luo, Xiaolin Xu, and Deliang Fan. 2021. Deep-Dup: An Adversarial Weight Duplication Attack Framework to Crush Deep Neural Network in Multi-Tenant FPGA. In 30th USENIX Security Symposium (USENIX Security 21). USENIX Association, 1919\u20131936. https:\/\/www.usenix.org\/conference\/usenixsecurity21\/presentation\/rakin"},{"key":"e_1_3_1_63_2","unstructured":"Hadi Salman Greg Yang Huan Zhang Cho-Jui Hsieh and Pengchuan Zhang. 2019. A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks. In Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019 NeurIPS 2019 December 8-14 2019 Vancouver BC Canada Hanna M. Wallach Hugo Larochelle Alina Beygelzimer Florence d\u2019Alch\u00e9-Buc Emily B. Fox and Roman Garnett (Eds.). 9832\u20139842. https:\/\/proceedings.neurips.cc\/paper\/2019\/hash\/246a3c5544feb054f3ea718f61adfa16-Abstract.html"},{"key":"e_1_3_1_64_2","unstructured":"Gagandeep Singh Timon Gehr Matthew Mirman Markus P\u00fcschel and Martin T. Vechev. 2018. Fast and Effective Robustness Certification. In Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018 NeurIPS 2018 December 3-8 2018 Montr\u00e9al Canada Samy Bengio Hanna M. Wallach Hugo Larochelle Kristen Grauman Nicol\u00f2 Cesa-Bianchi and Roman Garnett (Eds.). 10825\u201310836. https:\/\/proceedings.neurips.cc\/paper\/2018\/hash\/f2f446980d8e971ef3da97af089481c3-Abstract.html"},{"key":"e_1_3_1_65_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290354"},{"key":"e_1_3_1_66_2","doi-asserted-by":"publisher","DOI":"10.1002\/INT.22510"},{"key":"e_1_3_1_67_2","doi-asserted-by":"publisher","DOI":"10.1109\/TPAMI.2022.3181972"},{"key":"e_1_3_1_68_2","doi-asserted-by":"publisher","DOI":"10.1109\/DSN58367.2023.00023"},{"key":"e_1_3_1_69_2","doi-asserted-by":"publisher","DOI":"10.1109\/DSN58367.2023.00023"},{"key":"e_1_3_1_70_2","doi-asserted-by":"publisher","unstructured":"Hoang-Dung Tran Stanley Bak Weiming Xiang and Taylor T. Johnson. 2020. Verification of Deep Convolutional Neural Networks Using ImageStars. In Proceedings of the International Conference on Computer Aided Verification. 18\u201342. https:\/\/doi.org\/10.1007\/978-3-030-53288-8_2 10.1007\/978-3-030-53288-8_2","DOI":"10.1007\/978-3-030-53288-8_2"},{"key":"e_1_3_1_71_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30942-8_39"},{"key":"e_1_3_1_72_2","doi-asserted-by":"publisher","DOI":"10.1109\/TED.2021.3060362"},{"key":"e_1_3_1_73_2","first-page":"1599","volume-title":"27th USENIX Security Symposium, USENIX Security 2018, Baltimore, MD, USA, August 15-17, 2018","author":"Wang Shiqi","year":"2018","unstructured":"Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. 2018. Formal Security Analysis of Neural Networks using Symbolic Intervals. In 27th USENIX Security Symposium, USENIX Security 2018, Baltimore, MD, USA, August 15-17, 2018, William Enck and Adrienne Porter Felt (Eds.). USENIX Association, 1599\u20131614. https:\/\/www.usenix.org\/conference\/usenixsecurity18\/presentation\/wang-shiqi"},{"key":"e_1_3_1_74_2","unstructured":"Shiqi Wang Huan Zhang Kaidi Xu Xue Lin Suman Jana Cho-Jui Hsieh and J. Zico Kolter. 2021. Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Neural Network Robustness Verification. In Advances in Neural Information Processing Systems 34: Annual Conference on Neural Information Processing Systems 2021 NeurIPS 2021 December 6-14 2021 virtual Marc\u2019Aurelio Ranzato Alina Beygelzimer Yann N. Dauphin Percy Liang and JenniferWortman Vaughan (Eds.). 29909\u201329921. https:\/\/proceedings.neurips.cc\/paper\/2021\/hash\/fac7fead96dafceaf80c1daffeae82a4-Abstract.html"},{"key":"e_1_3_1_75_2","doi-asserted-by":"publisher","DOI":"10.1609\/AAAI.V34I04.6105"},{"key":"e_1_3_1_76_2","first-page":"1198","volume-title":"Proceedings of the Thirty-Sixth Conference on Uncertainty in Artificial Intelligence, UAI 2020, virtual online, August 3-6, 2020 (Proceedings of Machine Learning Research, Vol. 124)","author":"Wicker Matthew","year":"2020","unstructured":"Matthew Wicker, Luca Laurenti, Andrea Patane, and Marta Kwiatkowska. 2020. Probabilistic Safety for Bayesian Neural Networks. In Proceedings of the Thirty-Sixth Conference on Uncertainty in Artificial Intelligence, UAI 2020, virtual online, August 3-6, 2020 (Proceedings of Machine Learning Research, Vol. 124), Ryan P. Adams and Vibhav Gogate (Eds.). AUAI Press, 1198\u20131207. http:\/\/proceedings.mlr.press\/v124\/wicker20a.html"},{"key":"e_1_3_1_77_2","unstructured":"WikiChip. Accessed April 30 2022. FSD Chip - Tesla. https:\/\/en.wikichip.org\/wiki\/tesla_(car_company)\/fsd_chip."},{"key":"e_1_3_1_78_2","volume-title":"9th International Conference on Learning Representations, ICLR 2021, Virtual Event, Austria, May 3-7, 2021","author":"Xu Kaidi","year":"2021","unstructured":"Kaidi Xu, Huan Zhang, Shiqi Wang, Yihan Wang, Suman Jana, Xue Lin, and Cho-Jui Hsieh. 2021. Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers. In 9th International Conference on Learning Representations, ICLR 2021, Virtual Event, Austria, May 3-7, 2021. OpenReview.net. https:\/\/openreview.net\/forum?id=nVZtXBI6LNn"},{"key":"e_1_3_1_79_2","doi-asserted-by":"publisher","DOI":"10.1109\/HPCA51647.2021.00037"},{"key":"e_1_3_1_80_2","doi-asserted-by":"publisher","unstructured":"Pengfei Yang Renjue Li Jianlin Li Cheng-Chao Huang Jingyi Wang Jun Sun Bai Xue and Lijun Zhang. 2021. Improving Neural Network Verification through Spurious Region Guided Refinement. In Proceedings of 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) Jan Friso Groote and Kim Guldstrand Larsen (Eds.). 389\u2013408. https:\/\/doi.org\/10.1007\/978-3-030-72016-2_21 10.1007\/978-3-030-72016-2_21","DOI":"10.1007\/978-3-030-72016-2_21"},{"key":"e_1_3_1_81_2","first-page":"1463","volume-title":"29th USENIX Security Symposium, USENIX Security 2020, August 12-14, 2020","author":"Yao Fan","year":"2020","unstructured":"Fan Yao, Adnan Siraj Rakin, and Deliang Fan. 2020. DeepHammer: Depleting the Intelligence of Deep Neural Networks through Targeted Chain of Bit Flips. In 29th USENIX Security Symposium, USENIX Security 2020, August 12-14, 2020, Srdjan Capkun and Franziska Roesner (Eds.). USENIX Association, 1463\u20131480. https:\/\/www.usenix.org\/conference\/usenixsecurity20\/presentation\/yao"},{"key":"e_1_3_1_82_2","doi-asserted-by":"publisher","DOI":"10.1137\/22M1511709"},{"key":"e_1_3_1_83_2","doi-asserted-by":"publisher","unstructured":"Yedi Zhang Guangke Chen Fu Song Jun Sun and Jin Song Dong. 2024. Certified Quantization Strategy Synthesis for Neural Networks. In Proceedings of the 26th International Symposium on Formal Methods (FM) Part I Andr\u00e9 Platzer Kristin Yvonne Rozier Matteo Pradella and Matteo Rossi (Eds.) Vol. 14933. 343\u2013362. https:\/\/doi.org\/10.1007\/978-3-031-71162-6_18 10.1007\/978-3-031-71162-6_18","DOI":"10.1007\/978-3-031-71162-6_18"},{"key":"e_1_3_1_84_2","unstructured":"Yedi Zhang Lei Huang Pengfei Gao Fu Song Jun Sun and Jin Song Dong. 2025. Verification of Bit-Flip Attacks against Quantized Neural Networks. arXiv:2502.16286 [cs.CR] https:\/\/arxiv.org\/abs\/2502.16286"},{"key":"e_1_3_1_85_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37703-7_20"},{"key":"e_1_3_1_86_2","doi-asserted-by":"publisher","unstructured":"Yedi Zhang Zhe Zhao Guangke Chen Fu Song and Taolue Chen. 2021. BDD4BNN: A BDD-Based Quantitative Analysis Framework for Binarized Neural Networks. In Proceedings of the 33rd International Conference on Computer Aided Verification (CAV). 175\u2013200. https:\/\/doi.org\/10.1007\/978-3-030-81685-8_8 10.1007\/978-3-030-81685-8_8","DOI":"10.1007\/978-3-030-81685-8_8"},{"key":"e_1_3_1_87_2","doi-asserted-by":"publisher","DOI":"10.1145\/3563212"},{"key":"e_1_3_1_88_2","doi-asserted-by":"publisher","unstructured":"Yedi Zhang Zhe Zhao Guangke Chen Fu Song Min Zhang Taolue Chen and Jun Sun. 2022. QVIP: An ILP-based Formal Verification Approach for Quantized Neural Networks. In Proceedings of the 37th IEEE\/ACM International Conference on Automated Software Engineering (ASE). 82:1\u201382:13. https:\/\/doi.org\/10.1145\/3551349.3556916 10.1145\/3551349.3556916","DOI":"10.1145\/3551349.3556916"},{"key":"e_1_3_1_89_2","doi-asserted-by":"publisher","DOI":"10.1145\/3631977"},{"key":"e_1_3_1_90_2","doi-asserted-by":"publisher","unstructured":"Zhe Zhao Yedi Zhang Guangke Chen Fu Song Taolue Chen and Jiaxiang Liu. 2022. CLEVEREST: Accelerating CEGAR-based Neural Network Verification via Adversarial Attacks. In Proceedings of the 29th International Symposium on Static Analysis. 449\u2013473. https:\/\/doi.org\/10.1007\/978-3-031-22308-2_20 10.1007\/978-3-031-22308-2_20","DOI":"10.1007\/978-3-031-22308-2_20"},{"key":"e_1_3_1_91_2","volume-title":"5th International Conference on Learning Representations, ICLR 2017, Toulon, France, April 24-26, 2017, Conference Track Proceedings","author":"Zhou Aojun","year":"2017","unstructured":"Aojun Zhou, Anbang Yao, Yiwen Guo, Lin Xu, and Yurong Chen. 2017. Incremental Network Quantization: Towards Lossless CNNs with Low-precision Weights. In 5th International Conference on Learning Representations, ICLR 2017, Toulon, France, April 24-26, 2017, Conference Track Proceedings. OpenReview.net. https:\/\/openreview.net\/forum?id=HyQJ-mclg"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720471","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3720471","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T16:30:31Z","timestamp":1787589031000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720471"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,9]]},"references-count":90,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2025,4,9]]}},"alternative-id":["10.1145\/3720471"],"URL":"https:\/\/doi.org\/10.1145\/3720471","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,4,9]]},"assertion":[{"value":"2024-10-15","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-02-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-04-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}