Publications

Edited Volumes

  1. Preface to Special Issue on System Software Security (Chinese). Min Yang, Chao Zhang, Fu Song and Yuan Zhang Journal of Software, 2022, 33(6): 195-1960
  2. Preface to Special Issue on System Software Security. Min Yang, Chao Zhang, Fu Song and Yuan Zhang International Journal of Software and Informatics, 2022, 12(3): 259-261

Books and Book Articles

  1. Research Progress and Trends on Domain-Specific Modeling and Formal Verification of Safety Critical Systems. Dianfu Ma, Wensheng Niu, Sheng Cheng, Zhong Ma, Fu Song, Jie Luo, Ning Ge, Ping Lu, Ming Mu, Chuang Wang, Huaqiang Qiu, Yibin Tang and Xinfa Dai. CCF 2020-2021 Progress Report on Chinese Computer Science and Technology. China Machine Press, pages 141-189, 2021.
  2. Research Progress and Trends on Formal Verification of Artificial Intelligence Systems. Lei Bu, Liqian Chen, Yunwei Dong, Xiaowei Huang, Jianlin Li, Qin Li, Wanwei Liu, Wenjian Ruan, Fu Song, Youcheng Sun, Jingyi Wang, Min Wu, Zhiwu Xu, Bai Xue, Pengfei Yang, Xinping Yi, Lijun Zhang and Min Zhang. CCF 2019-2020 Progress Report on Chinese Computer Science and Technology. China Machine Press, pages 491-539, 2020.
  3. Research Progress and Trends on Formal Methods. Lei Bu, Liqian Chen, Zhe Chen, Zhenbang Chen, Xinyu Feng, Yuan Feng, Fei He, Guoqiang Li, Wanwei Liu, Feifei Ma, Fu Song, Cong Tian, Shuling Wang, Zhilin Wu, Bai Xue, Pengfei Yang, Liangze Yin, Bohua Zhan, Min Zhang, Lijun Zhang, Xingyuan Zhang and Yongwang Zhao. CCF 2017-2018 Progress Report on Chinese Computer Science and Technology. China Machine Press, pages 1-68, 2018.
  4. Formal Reasoning About Infinite Data Values: An Ongoing Quest (Invited survey). Taolue Chen, Fu Song, and Zhilin Wu. The 2nd International School on Engineering Trustworthy Software Systems (SETTS'16). 2016.

Refereed Journal Articles

  1. Qualitative and Quantitative Model Checking against Recurrent Neural Networks. Zhen Liang, Wanwei Liu, Fu Song, Bai Xue, Wenjing Yang, Ji Wang and Zhengbin Pang. Journal of Computer Science and Technology, 2023. (SCI, EI, CCF-B, CAS-JCR-Q2)
  2. Towards Understanding and Mitigating Audio Adversarial Examples for Speaker Recognition. Guangke Chen, Zhe Zhao, Fu Song*, Sen Chen, Lingling Fan, Feng Wang, and Jiashui Wang. IEEE Transactions on Dependable and Secure Computing, 2022. (SCI, EI, CCF-A, CAS-JCR-Q1)
  3. Precise Quantitative Analysis of Binarized Neural Networks: A BDD-based Approach. Yedi Zhang, Zhe Zhao, Guangke Chen, Fu Song* and Taolue Chen. ACM Transactions on Software Engineering and Methodology, 2022. (SCI, EI, CCF-A, CAS-JCR-Q1)
  4. AS2T: Arbitrary Source-To-Target Adversarial Attack on Speaker Recognition Systems. Guangke Chen, Zhe Zhao, Fu Song*, Sen Chen, Lingling Fan, and Yang Liu. IEEE Transactions on Dependable and Secure Computing, 2022. (SCI, EI, CCF-A, CAS-JCR-Q1)
  5. ESampler: Boosting sampling of satisfying assignments for Boolean formulas via derivation. Yongjie Xu, Fu Song* and Taolue Chen. Journal of Systems Architecture, 2022. (SCI, EI, CCF-B, CAS-JCR-Q2)
  6. VenomAttack: Automated and Adaptive Activity Hijacking in Android. Pu Sun, Sen Chen, Lingling Fan, Pengfei Gao, Fu Song* and Min Yang. Frontiers of Computer Science, volume 17(1):171801, pages 1-18, 2023. (SCI, EI, CCF-B, CAS-JCR-Q2)
  7. Taking Care of The Discretization Problem: A Comprehensive Study of the Discretization Problem and A Black-Box Adversarial Attack in Discrete Integer Domain. Lei Bu, Zhe Zhao, Yuchao Duan, and Fu Song*. IEEE Transactions on Dependable and Secure Computing, 2021. (SCI, EI, CCF-A, CAS-JCR-Q1)
  8. Model-based Automated Testing of JavaScript Web Applications via Longer Test Sequences. Pengfei Gao, Yongjie Xu, Fu Song* and Taolue Chen. Frontiers of Computer Science, volume 16(3):163204, pages 1-14, 2022. (SCI, EI, CCF-B, CAS-JCR-Q2)
  9. Formal Verification of Masking Countermeasures for Arithmetic Programs. Pengfei Gao, Hongyi Xie, Pu Sun, Jun Zhang, Fu Song* and Taolue Chen. IEEE Transactions on Software Engineering, volume 48(3), pages 973-1000, 2022. (SCI, EI, CCF-A, CAS-JCR-Q1)
  10. Advanced Evasion Attacks and Mitigations on Practical ML-Based Phishing Website Classifiers. Fu Song*, Yusi Lei, Sen Chen, Lingling Fan, and Yang Liu. International Journal of Intelligent Systems, volume 36(9), pages 5210-5240, 2021. (SCI, EI, CAS-JCR-Q2)
  11. A Hybrid Approach to Formal Verification of Higher-Order Masked Arithmetic Programs. Pengfei Gao, Hongyi Xie, Fu Song* and Taolue Chen. ACM Transactions on Software Engineering and Methodology, volume 30(3), pages 1-42, 2021. (SCI, EI, CCF-A)
  12. Verifying ReLU Neural Networks from a Model Checking Perspective. WanWei Liu, Fu Song, TangHaoRan Zhang and Ji Wang. Journal of Computer Science and Technology, volume 35(6), pages 1365-1381, 2020. (SCI, EI, CCF-B, CAS-JCR-Q2)
  13. Making Agents' Abilities Explicit. Yedi Zhang, Fu Song* and Taolue Chen. IEEE Access, volume 7, pages 101804-101819, 2019. (SCI, EI, CAS-JCR-Q2)
  14. Verifying and Quantifying Side-Channel Resistance of Masked Software Implementations. Pengfei Gao, Jun Zhang, Fu Song* and Chao Wang. ACM Transactions on Software Engineering and Methodology, volume 28(3), pages 16:1-16:32, 2019. (SCI, EI, CCF-A)
  15. Fuzzy Pushdown Termination Games. Haiyu Pan, Fu Song, Yongzhi Cao, and Junyan Qian. IEEE Transactions on Fuzzy Systems, volume 27(4), pages 760-774, 2019. (SCI, EI, CAS-JCR-Q1)
  16. Analyzing Pushdown Systems with Stack Manipulation. Fu Song. Information and Computation, volume 259(1), pages 41-71, 2018. (SCI, EI, CCF-A)
  17. Towards Backbone Computing: A Greedy-Whitening Based Approach. Yueling Zhang, Min Zhang, Geguang Pu, Fu Song and Jianwen Li. AI Communications, volume 31(3), pages 267-280, 2018. (SCI, EI)
  18. Model-Checking for Heterogeneous Multi-agent Systems (In Chinese). Yedi Zhang and Fu Song. Journal of Software (JOS), volume 29(6), 2018. (EI, CCF-A)
  19. On the Complexity of Omega-Pushdown Automata. Yusi Lei, Wanwei Liu, Min Zhang and Fu Song*. SCIENCE CHINA Information Sciences, volume 60(11), pages 112102:1-112102:15, 2017. (SCI, EI, CCF-A, CAS-JCR-Q2)
  20. On Temporal Logics with Data Variable Quantifications: Decidability and Complexity. Fu Song and Zhilin Wu. Information and Computation, volume 251, pages 104-139, 2016. (SCI, EI, CCF-A)
  21. Model-checking software library API usage rules. Fu Song and Tayssir Touili. Software and Systems Modeling, volume 15(4), pages 961-985, 2016. (SCI, EI, CCF-B, CAS-JCR-Q2)
  22. An Improved Online/Offline Identity-Based Signature Scheme for WSNs. Ya Gao, Peng Zeng, Kim-Kwang Raymond Choo and Fu Song. Journal of Network Security, volume 18(6), pages 1143-1151, November 2016. (EI)
  23. Survey on Formal Models to Reason about Infinite Data Values (In Chinese). Fu Song and Zhilin Wu. Journal of Software, Volume 27(3):a14, March 2016. (EI, CCF-A)
  24. Model Checking Dynamic Pushdown Networks. Formal Aspects of Computing, volume 27(2), Pages 397-421, March 2015. Fu Song and Tayssir Touili. (SCI, EI, CCF-B)
  25. Efficient CTL Model-Checking for Pushdown Systems. Fu Song and Tayssir Touili. Theoretical Computer Science, volume 549, Pages 127-145, September 2014. (SCI, EI, CCF-B)
  26. Pushdown Model-Checking for Malware Detection. Fu Song and Tayssir Touili. Journal on Software Tools for Technology Transfer, volume 16(2), Pages 147-173, April 2014. (SCI, EI, CCF-C)

Refereed Conference and Workshop Articles

  1. An Automata-Theoretic Approach to Synthesizing Binarized Neural Networks. Ye Tao, Wanwei Liu, Fu Song*, Zhen Liang, Ji Wang and Hongxu Zhu. Proceedings of the 21st International Symposium on Automated Technology for Verification and Analysis (ATVA), 2023. (EI, CCF-C)
  2. QFA2SR: Query-Free Adversarial Transfer Attacks to Speaker Recognition Systems. Guangke Chen, Yedi Zhang, Zhe Zhao and Fu Song*. Proceedings of the 32nd USENIX Security Symposium, 2023. (EI, CCF-A)
  3. CodeMark: Imperceptible Watermarking for Code Datasets against Neural Code Completion Models. Zhensu Sun, Xiaoning Du, Fu Song and Li Li. Proceedings of the 31th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE), 2023. (EI, CCF-A)
  4. QEBVerif: Quantization Error Bound Verification of Neural Networks. Yedi Zhang, Fu Song* and Jun Sun. Proceedings of the 35th International Conference on Computer Aided Verification (CAV), 2023. (EI, CCF-A)
  5. Automated Verification of Correctness for Masked Arithmetic Programs. Mingyang Liu, Fu Song* and Taolue Chen. Proceedings of the 35th International Conference on Computer Aided Verification (CAV), 2023. (EI, CCF-A)
  6. SCAGuard: Detection and Classification of Cache Side-Channel Attacks via Attack Behavior Modeling and Similarity Comparison. Limin Wang, Lei Bu and Fu Song. Proceedings of the 59th ACM/IEEE Design Automation Conference (DAC), 2023. (EI, CCF-A)
  7. Don't Complete It! Preventing Unhelpful Code Completion for Productive and Sustainable Neural Code Completion Systems. Zhensu Sun, Xiaoning Du, Fu Song, Shangwen Wang, Mingze Ni and Li Li. Proceedings of the 44th IEEE/ACM International Conference on Software Engineering (ICSE), 2023. (EI)
  8. QVIP: An ILP-based Formal Verification Approach for Quantized Neural Networks. Yedi Zhang, Zhe Zhao, Guangke Chen, Fu Song*, Min Zhang and Taolue Chen. Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering (ASE), 2022. (EI, CCF-A)
  9. Accelerating CEGAR-based Neural Network Verification via Adversarial Attacks. Zhe Zhao, Yedi Zhang, Guangke Chen, Fu Song*, Taolue Chen and Jiaxiang Liu. Proceedings of the 29th Static Analysis Symposium (SAS), 2022. (EI, CCF-B)
  10. DeJITLeak: Eliminating JIT-Induced Timing Side-Channel Leaks. Qi Qin, JulianAndres JiYang, Fu Song*, Taolue Chen and Xinyu Xing. Proceedings of the 21st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE), 2022. Won the Distinguished Paper Award at the CIE Conference on Cyber Security 2023. (EI, CCF-A)
  11. PoS4MPC: Automated Security Policy Synthesis Secure Multi-Party Computation. Yuxin Fan, Fu Song*, Taoulue Chen, Liangfeng Zhang and Wanwei Liu. Proceedings of the 33rd International Conference on Computer Aided Verification (CAV), 2022. (EI, CCF-A)
  12. CoProtector: Protect Open-Source Code against Unauthorized Training Usage with Data Poisoning. Zhensu Sun, Xiaoning Du, Fu Song, Mingze Ni and Li Li. Proceedings of the ACM Web Conference (WWW), 2022. (EI, CCF-A)
  13. ESAMPLER: Efficient Sampling of Satisfying Assignments for Boolean Formulas. Yongjie Xu, Fu Song* and Taolue Chen. Proceedings of the 7th Symposium on Dependable Software Engineering Theories, Tools and Applications (SETTA), 2021. (EI)
  14. Locality based Cache Side Channel Attack Detection. Limin Wang, Lei Bu and Fu Song. Proceedings of the the 10th International Workshop on Security Proofs for Embedded Systems (PROOFS), 2021. (EI)
  15. Peeking into the Gray Area of Mobile World: An Empirical Study of Unlabeled Android Apps. Sen Chen, Lingling Fan, Cuiyun Gao, Fu Song and Yang Liu. Proceedings of the 32th International Symposium on Software Reliability Engineering (ISSRE), 2021. (EI, CCF-B)
  16. Eager Falsification For Accelerating Robustness Verification of Deep Neural Networks. Min Zhang, Wenjie Wan, Zhaodi Zhang, Fu Song, Xuejun Wen and Xingwu Guo. Proceedings of the 32th International Symposium on Software Reliability Engineering (ISSRE), 2021. (EI, CCF-B)
  17. BDD4BNN: A BDD-based Quantitative Analysis Framework for Binarized Neural Networks. Yedi Zhang, Zhe Zhao, Guangke Chen, Fu Song* and Taolue Chen. Proceedings of the 33rd International Conference on Computer Aided Verification (CAV), 2021. (EI, CCF-A)
  18. Attack as Defense: Characterizing Adversarial Examples using Robustness. Zhe Zhao, Guangke Chen, Jingyi Wang, Yiwei Yang, Fu Song* and Jun Sun. Proceedings of the 30th ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA), 2021. (EI, CCF-A)
  19. Inferring Loop Invariants for Multi-Path Loops. Yingwen Liu, Yao Zahng, Sen Chen, Fu Song, Xiaofei Xie, Xiaohong Li and Lintan Sun. Proceedings of the 15th International Symposium on Theoretical Aspects of Software Engineering (TASE), 2021. (EI, CCF-C)
  20. Who is Real Bob? Adversarial Attacks on Speaker Recognition Systems. Guangke Chen, Sen Chen, Lingling Fan, Xiaoning Du, Zhe Zhao, Fu Song* and Yang Liu. Proceedings of the 42nd IEEE Symposium on Security and Privacy (IEEE S&P), 2021. (EI, CCF-A)
  21. Patch Based Vulnerability Matching for Binary Programs. Yifei Xu, Zhengzi Xu, Bihuan Chen, Fu Song, Yang Liu and Ting Liu. Proceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA), 2020. (EI, CCF-A)
  22. Android Malware Family Classification and Characterization Using CFG and DFG. Zhiwu Xu, Kerong Ren and Fu Song. Proceedings of the 13th International Symposium on Theoretical Aspects of Software Engineering (TASE), 2019. (EI, CCF-C)
  23. Quantitative Verification of Masked Arithmetic Programs against Side-Channel Attacks. Pengfei Gao, Hongyi Xie, Jun Zhang, Fu Song* and Taolue Chen. Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (ETAPS/TACAS), Prague, Czech Republic. April 6-11, 2019. (EI, CCF-B)
  24. SMT-Based Bounded Schedulability Analysis of the Clock Constraint Specification Language. Min Zhang, Fu Song*, Frederic Mallet and Xiaohong Chen. Proceedings of the 22th International Conference on Theoretical Aspects of Software Engineering (ETAPS/FASE), Prague, Czech Republic. April 6-11, 2019. (EI, CCF-B)
  25. Probabilistic Alternating-Time Mu-Calculus. Fu Song, Yedi Zhang, Yu Tang, Taolue Chen and Zhiwu Xu. Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence (AAAI), Hawaii, USA. January 27-February 1, 2019. (CCF-A)
  26. KRust: A Formal Executable Semantics of Rust. Feng Wang, Fu Song, Min Zhang, Xiaoran Zhu and Jun Zhang. Proceedings of the 12th International Symposium on Theoretical Aspects of Software Engineering (TASE), 2018. (EI, CCF-C)
  27. SCInfer: Refinement-based Verification of Software Countermeasures against Side-Channel Attacks. Jun Zhang, Pengfei Gao, Fu Song* and Chao Wang. Proceedings of the 30th International Conference on Computer Aided Verification (CAV), Oxford, UK. July 14-17, 2018. (EI, CCF-A)
  28. Android Stack Machine. [Full version] Taolue Chen, Jinlong He, Fu Song, Guozhen Wang, Zhilin Wu and Jun Yan. Proceedings of the 30th International Conference on Computer Aided Verification (CAV), Oxford, UK. July 14-17, 2018. (EI, CCF-A)
  29. Reasoning about Periodicity on Infinite Words. Wanwei Liu, Fu Song and Ge Zhou. Proceedings of the 3rd Symposium on Dependable Software Engineering (SETTA). Changsha, China. October 23-25, 2017. (EI)
  30. Model Checking Pushdown Epistemic Game Structures. [Full version] Taolue Chen, Fu Song and Zhilin Wu. Proceedings of the 19th International Conference on Formal Engineering Methods (ICFEM). Xi'an, China. November 13-17, 2017. (EI, CCF-C)
  31. Tractability of separation logic with inductive definitions: Beyond lists. Taolue Chen, Fu Song and Zhilin Wu. Proceedings of the 28th International Conference on Concurrency Theory (CONCUR). Berlin, Germany. September 5-8, 2017. (EI, CCF-B)
  32. Optimizing Backbone Filtering. Yueling Zhang, Jianwen Li, Min Zhang, Geguang Pu and Fu Song. Proceedings of the 11th International Symposium on Theoretical Aspects of Software Engineering (TASE). Nice, France, September 13-15, 2017. (EI, CCF-C)
  33. SPAIN: Security Patch Analysis for Binaries - Towards Understanding the Pain and Pills. Zhengzi Xu, Bihuan Chen, Mahinthan Chandramohan, Yang Liu and Fu Song. Proceedings of the 39th ACM/IEEE International Conference on Software Engineering (ICSE). Buenos Aires, Argentina, May 20-28, 2017. (EI, CCF-A)
  34. Verifying Pushdown Multi-Agent Systems against Strategy Logics. Taolue Chen, Fu Song* and Zhilin Wu. Proceedings of the 25th International Joint Conference on Artifficial Intelligence (IJCAI). New York, USA. 9-15 July, 2016. (EI, CCF-A,Oral presentation)
  35. Global Model Checking on Pushdown Multi-Agent Systems. Taolue Chen, Fu Song* and Zhilin Wu. Proceedings of the 30th AAAI Conference on Artifficial Intelligence (AAAI). Arizona, USA. 12-17 February, 2016. (EI, CCF-A, Oral presentation)
  36. On Reachability Analysis of Pushdown Systems with Transductions: Application to Boolean Programs with Call-by-Reference. Fu Song, Weikai Miao, Geguang Pu and Min Zhang. Proceedings of the 26th International Conference on Concurrency Theory (CONCUR). Madrid, Spain. September 1-4, 2015. (EI, CCF-B)
  37. On the Satisfiability of Indexed Linear Temporal Logics. Taolue Chen, Fu Song* and Zhilin Wu. Proceedings of the 26th International Conference on Concurrency Theory (CONCUR). Madrid, Spain. 1-4 September, 2015. (EI, CCF-B)
  38. Modeling and Verifying Google File System. Bo Li, Mengdi Wang, Yongxin Zhao, Geguang Pu, Huibiao Zhu and Fu Song. Proceedings of 16th IEEE International Symposium on High Assurance Systems Engineering (HASE). Daytona Beach, FL, USA. 8-10 January, 2015. (EI)
  39. Extending temporal logics with data variable quantifications. Fu Song and Zhilin Wu. Proceedings of the 34th Foundations of Software Technology and Theoretical Computer Science (FSTTCS). New Delhi, India. 15-17 December, 2014. (EI, CCF-C)
  40. Model Checking for Android Malware Detection. Fu Song and Tayssir Touili. Proceedings of the 12th Asian Symposium on Programming Languages and Systems (APLAS). Singapore. 17-19 November, 2014. (EI, CCF-C)
  41. Model Checking Dynamic Pushdown Networks. Fu Song and Tayssir Touili. Proceedings of the 11th Asian Symposium on Programming Languages and Systems (APLAS). Melbourne, Australia. 9-11 December, 2013. (EI, CCF-C)
  42. POMMADE:PushdOwn Model-checking for Malware DEtection. Fu Song and Tayssir Touili. Proceedings of the 9th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE). Russia. August 18-26, 2013. (EI, CCF-A)
  43. Model-Checking Software Library API Usage Rules. Fu Song and Tayssir Touili. Proceedings of the 10th International Conference on integrated Formal Methods (iFM). Turku, Finland. June 10-14, 2013. (EI)
  44. LTL Model-Checking For Malware Detection. Fu Song and Tayssir Touili. Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Rome, Italy. March 16-24, 2013. (EI, CCF-B)
  45. PuMoC: A CTL Model-Checker For Sequential Programs. Fu Song and Tayssir Touili. Proceedings of the 27th IEEE/ACM International Conference On Automated Software Engineering (ASE). Essen, Germany. 3-7 September 2012. (EI, CCF-A)
  46. Efficient Malware Detection Using Model-Checking. Fu Song and Tayssir Touili. Proceedings of the 18th International Symposium on Formal Methods (FM). Paris, France. 27-31 Aug. 2012. (EI, CCF-A)
  47. Pushdown Model-Checking for Malware Detection. Fu Song and Tayssir Touili. Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Tallinn, Estonia. March 24-April 1, 2012. Won the EASST Best Paper Award at ETAPS 2012. (EI, CCF-B)
  48. Efficient CTL Model-Checking for Pushdown Systems. Fu Song and Tayssir Touili. Proceedings of the International Conference on Concurrency Theory (CONCUR). Aachen, Germany. 6-9 September 2011. (EI, CCF-B)
  49. A Distributed Clustering Algorithm for Voronoi Cell-based Large Scale Wireless Sensor Network. Jiehui Chen, Chulsoo Kim and Fu Song. the International Conference on Communications and Mobile Computing (IEEE CMC). Shenzhen, China. 12-14 April 2010. (EI)
  50. Integrating the B-method into PVS. Jiaming Zhou, Jian Guo and Fu Song. the International Conference on Information Engineering and Computer Science (ICIECS). Wuhan, China. 19-20 Dec. 2009. (EI)