Publications
2025
- Verification of Bit-Flip Attacks against Quantized Neural Networks
Yedi Zhang and Lei Huang and Pengfei Gao and Fu Song and Jun Sun and Jin Song Dong, Object-Oriented Programming Systems, Languages and Applications (OOPSLA), 2025.
- Training Verification-Friendly Neural Networks via Neuron Behavior Consistency
Zongxin Liu and Zhe Zhao and Fu Song and Jun Sun and Pengfei Yang and Xiaowei Huang and Lijun Zhang, Thirty-Ninth AAAI Conference on Artificial Intelligence (AAAI-25), 2025. DOI
- An Efficient String Solver for String Constraints with Regex-Counting and String-Length
Denghang Hu and Zhilin Wu, Journal of Systems Architecture, 2025. DOI
- SongBsAb: A Dual Prevention Approach against Singing Voice Conversion based Illegal Song Covers
Guangke Chen and Yedi Zhang and Fu Song and Ting Wang and Xiaoning Du and Yang Liu, Proceedings of the 32nd Annual Network and Distributed System Security Symposium (NDSS) (Accepted), 2025.
- LaserGuider: A Laser Based Physical Backdoor Attack against Deep Neural Networks
Yongjie Xu and Guangke Chen and Fu Song and Yuqi Chen, Network Security (ACNS), 2025.
- Formalization of Android Activity-Fragment Multitasking Mechanism and Static Analysis of Mobile Apps
Jinlong He and Zhilin Wu and Taolue Chen, Formal Aspects of Computing, 2025. DOI
2024
- Don't Complete It! Preventing Unhelpful Code Completion for Productive and Sustainable Neural Code Completion Systems
Zhensu Sun and Xiaoning Du and Fu Song and Shangwen Wang and Mingze Ni and Li Li and David Lo, ACM Transactions on Software Engineering and Methodology (Accepted), 2024.
- Formal Verification of RISC-V Processor Chisel Designs
Shidong Shen and Yicheng Liu and Lijun Zhang and Fu Song and Zhilin Wu, Dependable Software Engineering. Theories, Tools, and Applications, 2024. DOI
- Molecular Graph Representation Learning via Structural Similarity Information
Chengyu Yao and Hong Huang and Hang Gao and Fengge Wu and Haiming Chen and Junsuo Zhao, Joint European Conference on Machine Learning and Knowledge Discovery in Databases, 2024. DOI
- Towards an Effective Method of ReDoS Detection for Non-backtracking Engines
Weihao Su and Hong Huang and Rongchen Li and Haiming Chen and Tingjian Ge, 33rd USENIX Security Symposium (USENIX Security 24), 2024.
- Verifying Randomized Consensus Protocols with Common Coins
Song Gao and Bohua Zhan and Zhilin Wu and Lijun Zhang, 2024 54th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN), 2024. DOI
- SLMIA-SR: Speaker-Level Membership Inference Attacks against Speaker Recognition Systems
Guangke Chen and Yedi Zhang and Fu Song, Proceedings of the 31st Annual Network and Distributed System Security (NDSS) Symposium, 2024.
- FDI: Attack Neural Code Generation Systems through User Feedback Channel
Zhensu Sun and Xiaoning Du and Xiapu Luo and Fu Song and David Lo and Li Li, Proceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis, 2024. DOI
- SAT-based Formal Verification of Fault Injection Countermeasures for Cryptographic Circuits
Huiyu Tan and Pengfei Gao and Fu Song and Taolue Chen and Zhilin Wu, IACR Transactions on Cryptographic Hardware and Embedded Systems, 2024. DOI
- Formally Verifying Arithmetic Chisel Designs for All Bit Widths at Once
Weizhi Feng and Yicheng Liu and Jiaxiang Liu and David N. Jansen and Lijun Zhang and Zhilin Wu, Proceedings of the 61st ACM/IEEE Design Automation Conference, 2024. DOI
- A decision procedure for string constraints with string/integer conversion
and flat regular constraints
Hao Wu and Yu-Fang Chen and Zhilin Wu and Bican Xia and Naijun Zhan, Acta Informatica, 2024. DOI
- When Neural Code Completion Models Size up the Situation: Attaining
Cheaper and Faster Completion through Dynamic Model Inference
Zhensu Sun and Xiaoning Du and Fu Song and Shangwen Wang and Li Li, Proceedings of the 46th IEEE/ACM International Conference on Software Engineering, ICSE 2024, Lisbon, Portugal, April 14-20, 2024, 2024. DOI
- Certified Quantization Strategy Synthesis for Neural Networks
Yedi Zhang and Guangke Chen and Fu Song and Jun Sun and Jin Song Dong, Formal Methods - 26th International Symposium, FM 2024, Milan, Italy, September 9-13, 2024, Proceedings, Part I, 2024. DOI
- Compositional Verification of Cryptographic Circuits Against Fault
Injection Attacks
Huiyu Tan and Xi Yang and Fu Song and Taolue Chen and Zhilin Wu, Formal Methods - 26th International Symposium, FM 2024, Milan, Italy, September 9-13, 2024, Proceedings, Part II, 2024. DOI
- K-RAPID: A Formal Executable Semantics of the RAPID Robot Programming
Language
Zichen Wang and Jingyi Wang and Fu Song and Kun Wang and Hongyi Pu and Peng Cheng, Proceedings of the 10th ACM Cyber-Physical System Security Workshop, CPSS 2024, Singapore, 2 July 2024, 2024. DOI
- Compositional Verification of First-Order Masking Countermeasures
against Power Side-Channel Attacks
Pengfei Gao and Fu Song and Taolue Chen, ACM Trans. Softw. Eng. Methodol., 2024. DOI
- Attack as Detection: Using Adversarial Attack Methods to Detect Abnormal
Examples
Zhe Zhao and Guangke Chen and Tong Liu and Taishan Li and Fu Song and Jingyi Wang and Jun Sun, ACM Trans. Softw. Eng. Methodol., 2024. DOI
- Towards Efficient Verification of Constant-Time Cryptographic Implementations
Luwei Cai and Fu Song and Taolue Chen, Proc. ACM Softw. Eng., 2024. DOI
- EasyBC: A Cryptography-Specific Language for Security Analysis of
Block Ciphers against Differential Cryptanalysis
Pu Sun and Fu Song and Yuqi Chen and Taolue Chen, Proc. ACM Program. Lang., 2024. DOI
- Automatic Verification of Cryptographic Block Function Implementations
with Logical Equivalence Checking
Li-Chang Lai and Jiaxiang Liu and Xiaomu Shi and Ming-Hsien Tsai and Bow-Yaw Wang and Bo-Yin Yang, Computer Security - ESORICS 2024 - 29th European Symposium on Research in Computer Security, Bydgoszcz, Poland, September 16-20, 2024, Proceedings, Part IV, 2024. DOI
- Abstraction and Refinement: Towards Scalable and Exact Verification
of Neural Networks
Jiaxiang Liu and Yunhan Xing and Xiaomu Shi and Fu Song and Zhiwu Xu and Zhong Ming, ACM Trans. Softw. Eng. Methodol., 2024. DOI
2023
- String Constraints with Regex-Counting and String-Length Solved More
Efficiently
Denghang Hu and Zhilin Wu, Dependable Software Engineering. Theories, Tools, and Applications - 9th International Symposium, SETTA 2023, Nanjing, China, November 27-29, 2023, Proceedings, 2023. DOI
- QFA2SR: Query-Free Adversarial Transfer Attacks to Speaker Recognition
Systems
Guangke Chen and Yedi Zhang and Zhe Zhao and Fu Song, 32nd USENIX Security Symposium, USENIX Security 2023, Anaheim, CA, USA, August 9-11, 2023, 2023.
- CodeMark: Imperceptible Watermarking for Code Datasets against Neural
Code Completion Models
Zhensu Sun and Xiaoning Du and Fu Song and Li Li, Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2023, San Francisco, CA, USA, December 3-9, 2023, 2023. DOI
- QEBVerif: Quantization Error Bound Verification of Neural Networks
Yedi Zhang and Fu Song and Jun Sun, Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part II, 2023. DOI
- Automated Verification of Correctness for Masked Arithmetic Programs
Mingyang Liu and Fu Song and Taolue Chen, Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part III, 2023. DOI
- An Automata-Theoretic Approach to Synthesizing Binarized Neural Networks
Ye Tao and Wanwei Liu and Fu Song and Zhen Liang and Ji Wang and Hongxu Zhu, Automated Technology for Verification and Analysis - 21st International Symposium, ATVA 2023, Singapore, October 24-27, 2023, Proceedings, Part I, 2023. DOI
- Compositional Verification of Efficient Masking Countermeasures against
Side-Channel Attacks
Pengfei Gao and Yedi Zhang and Fu Song and Taolue Chen and Francois-Xavier Standaert, Proc. ACM Program. Lang., 2023. DOI
- Rooted Divergence-Preserving Branching Bisimilarity is a Congruence
for Guarded CCS
Quan Sun and David N. Jansen and Xinxin Liu and Wei Zhang, Formal Aspects Comput., 2023. DOI
- llvm2CryptoLine: Verifying Arithmetic in Cryptographic C Programs
Ruiling Chen and Jiaxiang Liu and Xiaomu Shi and Ming-Hsien Tsai and Bow-Yaw Wang and Bo-Yin Yang, Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2023, San Francisco, CA, USA, December 3-9, 2023, 2023. DOI
- Certified Verification for Algebraic Abstraction
Ming-Hsien Tsai and Yu-Fu Fu and Jiaxiang Liu and Xiaomu Shi and Bow-Yaw Wang and Bo-Yin Yang, Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part III, 2023. DOI
- CoqCryptoLine: A Verified Model Checker with Certified Results
Ming-Hsien Tsai and Yu-Fu Fu and Jiaxiang Liu and Xiaomu Shi and Bow-Yaw Wang and Bo-Yin Yang, Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part II, 2023. DOI
2022
- Solving string constraints with Regex-dependent functions through
transducers with priorities and variables
Taolue Chen and Alejandro Flores-Lamas and Matthew Hague and Zhilei Han and Denghang Hu and Shuanglong Kan and Anthony W. Lin and Philipp Rümmer and Zhilin Wu, Proc. ACM Program. Lang., 2022. DOI
- CHA: Supporting SVA-Like Assertions in Formal Verification of Chisel
Programs (Tool Paper)
Shizhen Yu and Yifan Dong and Jiuyang Liu and Yong Li and Zhilin Wu and David N. Jansen and Lijun Zhang, Software Engineering and Formal Methods - 20th International Conference, SEFM 2022, Berlin, Germany, September 26-30, 2022, Proceedings, 2022. DOI
- Rooted Divergence-Preserving Branching Bisimilarity is a Congruence:
A Simpler Proof
David N. Jansen and Xinxin Liu, A Journey from Process Algebra via Timed Automata to Model Learning - Essays Dedicated to Frits Vaandrager on the Occasion of His 60th Birthday, 2022. DOI
- Deciding All Behavioral Equivalences at Once: A Game for Linear-Time-Branching-Time
Spectroscopy
Benjamin Bisping and David N. Jansen and Uwe Nestmann, Log. Methods Comput. Sci., 2022. DOI
2021
- Solving Not-Substring Constraint withFlat Abstraction
Parosh Aziz Abdulla and Mohamed Faouzi Atig and Yu-Fang Chen and Bui Phi Diep and Lukáš Holík and Denghang Hu and Wei-Lun Tsai and Zhilin Wu and Di-De Yen, Programming Languages and Systems - 19th Asian Symposium, APLAS 2021, Chicago, IL, USA, October 17-18, 2021, Proceedings, 2021. DOI
- Frontmatter: mining Android user interfaces at scale
Konstantin Kuznetsov and Chen Fu and Song Gao and David N. Jansen and Lijun Zhang and Andreas Zeller, ESEC/FSE '21: 29th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, Athens, Greece, August 23-28, 2021, 2021. DOI
- Formal Verification of Consensus in the Taurus Distributed Database
Song Gao and Bohua Zhan and Depeng Liu and Xuechao Sun and Yanan Zhi and David N. Jansen and Lijun Zhang, Formal Methods - 24th International Symposium, FM 2021, Virtual Event, November 20-26, 2021, Proceedings, 2021. DOI
2020
- Computing Linear Arithmetic Representation of Reachability Relation
of One-Counter Automata
Xie Li and Taolue Chen and Zhilin Wu and Mingji Xia, Dependable Software Engineering. Theories, Tools, and Applications - 6th International Symposium, SETTA 2020, Guangzhou, China, November 24-27, 2020, Proceedings, 2020. DOI
- Monadic Decomposition in Integer Linear Arithmetic
Matthew Hague and Anthony W. Lin and Philipp Rümmer and Zhilin Wu, Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part I, 2020. DOI
- A Decision Procedure for Path Feasibility of String Manipulating Programs
with Integer Data Type
Taolue Chen and Matthew Hague and Jinlong He and Denghang Hu and Anthony Widjaja Lin and Philipp Rümmer and Zhilin Wu, Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings, 2020. DOI
- An O(m log n) algorithm for branching bisimilarity on labelled transition
systems
David N. Jansen and Jan Friso Groote and Jeroen J. A. Keiren and Anton Wijs, Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part II, 2020. DOI
- Accelerated Verification of Parametric Protocols with Decision Trees
Yongjian Li and Taifeng Cao and David N. Jansen and Jun Pang and Xiaotao Wei, 38th IEEE International Conference on Computer Design, ICCD 2020, Hartford, CT, USA, October 18-21, 2020, 2020. DOI
- A Near-Linear-Time Algorithm for Weak Bisimilarity on Markov Chains
David N. Jansen and Jan Friso Groote and Ferry Timmers and Pengfei Yang, 31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference), 2020. DOI