期刊论文(*表示通信作者) [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, CCF-B,中科院SCI分区2区 [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, CCF-A ,中科院SCI分区1区 [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, CCF-A ,中科院SCI分区1区 [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, CCF-A ,中科院SCI分区1区 [5]ESampler: Boosting Sampling of Satisfying Assignments for Boolean Formulas via Derivation.Yongjie Xu,Fu Song*and Taolue Chen. Journal of Systems Architecture,129:102615,2022, CCF-B ,中科院SCI分区2区 [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, 17(1): 171801, 2023, CCF-C ,中科院SCI分区2区 [7]Taking Care of the Discretization Problem: A Comprehensive Study of the Discretization Problem and A Black-Box Adversarial Attack in Discrete Integer Domain. Bu Lei, Zhe Zhao, Yuchao Duan andFu Song*. IEEE Transactions on Dependable and Secure Computing, 2021, CCF-A ,中科院SCI分区1区 [8]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, 36(9):5210–5240, 2021,中科院SCI分区1区 [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, 48(3):973–1000, 2022, CCF-A ,中科院SCI分区1区 [10]A Hybrid Approach to Formal Verification of Higher-Order Masked Arithmetic Programs.Pengfei Gao, Yongyi Xie,Fu Song*and Taolue Chen. ACM Transactions on Software Engineering and Methodology, 30(3):1–42, 2021, CCF-A,中科院SCI分区1区 [11]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, 16(3):163204, 2021, CCF-C ,中科院SCI分区2区 [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, 35(6):1365–1381,2020, CCF-B ,中科院SCI分区2区 [13]Making Agents’ Abilities Explicit. Yedi Zhang,Fu Song*and Taolue Chen. IEEE Access 7: 101804–101819, 2019,中科院SCI分区3区 [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, 28(3), 16:1–16:32, 2019, CCF-A,中科院SCI分区1区 [15]Fuzzy Pushdown Termination Games. Haiyu Pan,Fu Song, Yongzhi Cao, and Junyan Qian. IEEE Transactions on Fuzzy Systems, 27(4): 760–774, 2019,中科院SCI分区1区 [16]Towards Backbone Computing: A Greedy-Whitening Based Approach. Yueling Zhang, Min Zhang, Geguang Pu,Fu Songand Jianwen Li. AI Communications, 31(3): 267–280, 2018 [17]Analyzing Pushdown Systems with Stack Manipulation.Fu Song*. Information and Computation, 259(1): 41–71, 2018, CCF-A [18]异构多智能体系统模型检查.张业迪、宋富.软件学报, 29(6):1–13, 2018, CCF-A [19]On the Complexity ofomega-Pushdown Automata. Yusi Lei, Wanwei Liu, Min Zhang andFu Song*. SCIENCE CHINA Information Sciences, 60:112102:1–112102:15, 2017, CCF-B ,中科院SCI分区2区 [20]On Temporal Logics with Data Variable Quantifications: Decidability and Complexity.Fu Songand Zhilin Wu (按姓排序). Information and Computation, 251:104–139, 2016, CCF-A ,中科院SCI分区2区 [21]面向无穷数据的形式模型综述.宋富、吴志林(按姓排序).软件学报, 27(3):a14, 2016, CCF-A [22]An Improved Online/Offline Identity-Based Signature Scheme for WSNs.Ya Gao, Peng Zeng, Kim-Kwang Raymond Choo andFu Song. Journal of Network Security (IJNS), 18(6):1143–1151, 2016 [23]Model-checking Software Library API Usage Rules.Fu Songand Tayssir Touili. Software and Systems Modeling, 15(4):961–985, 2016, CCF-B ,中科院SCI分区2区 [24]Model Checking Dynamic Pushdown Networks.Fu Songand Tayssir Touili. Formal Aspects of Computing, 27(2):397–421, 2015, CCF-B [25]Efficient CTL Model-Checking for Pushdown Systems.Fu Songand Tayssir Touili. Theoretical Computer Science, 549:127–145, 2014, CCF-B [26]Pushdown Model Checking for Malware Detection.Fu Songand Tayssir Touili. International Journal on Software Tools for Technology Transfer, 16(2):147–173, 2014, CCF-C
会议论文(*表示通信作者) [1]An Automata-Theoretic Approach to Synthesizing Binarized Neural Networks.Ye Tao, Wanwei Liu,Fu Song, Zhen Liang, Ji Wang and Hongxu Zhu.In Proc. of the 21st International Symposium on Automated Technology for Verification and Analysis (ATVA), 2023, CCF-C [2]QFA2SR: Query-Free Adversarial Transfer Attacks to Speaker Recognition Systems. Guangke Chen, Yedi Zhang, Zhe Zhao andFu Song*. In Proc. of the 32nd USENIX Security Symposium (Security), 2023, CCF-A [3]CodeMark: Imperceptible Watermarking for Code Datasets against Neural Code Completion Models.Zhensu Sun, Xiaoning Du,Fu Song*and Li Li. In Proc. of the 31th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE), 2023, CCF-A [4]QEBVerif: Quantization Error Bound Verification of Neural Networks. Yedi Zhang,Fu Song* and Jun Sun. In Proc. of the 35th International Conference on Computer Aided Verification (CAV), 2023, CCF-A [5]Automated Verification of Correctness for Masked Arithmetic Programs. Mingyang Liu,Fu Song*and Taolue Chen. In Proc. of the 35th International Conference on Computer Aided Verification (CAV), 2023, CCF-A [6]SCAGuard: Detection and Classification of Cache Side-Channel Attacks via Attack Behavior Modeling and Similarity Comparison. Limin Wang, Lei Bu andFu Song. In Proc. of the 59th ACM/IEEE Design Automation Conference (DAC), 2023, 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. In Proc. of the 44th IEEE/ACM International Conference on Software Engineering (ICSE), 2023 [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. In Proc. of the 37th IEEE/ACM International Conference on Automated Software Engineering (ASE), 2022, 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. In Proc. of the 29th Static Analysis Symposium (SAS), 2022, CCF-B [10]DeJITLeak: Eliminating JIT-Induced Timing Side-Channel Leaks.Qi Qin, JulianAndres JiYang,Fu Song*,Taolue Chen and Xinyu Xing. In Proc. of the 21st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE), 2022, CCF-A [11]PoS4MPC: Automated Security Policy Synthesis for Secure Multi-Party Computation.Yuxin Fan,Fu Song*, Taolue Chen, Liangfeng Zhang and Wanwei Liu. In Proc. of the 34rd International Conference on Computer Aided Verification (CAV), 2022, 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. In Proc. of The Web Conference (WWW), 2022, CCF-A [13]ESAMPLER: Efficient Sampling of Satisfying Assignments for Boolean Formulas. Yongjie Xu,Fu Song*and Taolue Chen. In Proc. of the 7th Symposium on Dependable Software Engineering Theories, Tools and Applications (SETTA), 2021, CCF-C [14]Locality based Cache Side Channel Attack Detection. Limin Wang, Lei Bu andFu Song. In Proc. of the 10th International Workshop on Security Proofs for Embedded Systems (PROOFS), 2021 [15]Peeking into the Gray Area of Mobile World: Empirical Investigation of Unlabeled Android Apps in Industry. Sen Chen, Lingling Fan, Cuiyun Gao,Fu Songand Yang Liu. In Proc. of the 32th International Symposium on Software Reliability Engineering (ISSRE), 2021, 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. In Proc. of the 32th International Symposium on Software Reliability Engineering (ISSRE), 2021, CCF-B [17]Attack as Defense: Characterizing Adversarial Examples using Robustness. Zhe Zhao, Guangke Chen, Jingyi Wang, Yiwei Yang,Fu Song*and Jun Sun. In Proc. of the 30th ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA), 2021, CCF-A [18]BDD4BNN: A BDD-based Quantitative Analysis Framework for Binarized Neural Networks. Yedi Zhang, Zhe Zhao, Guangke Chen,Fu Song*and Taolue Chen. In Proc. of the 33rd International Conference on Computer Aided Verification (CAV), 2021, CCF-A [19]Inferring Loop Invariants for Multi-Path Loops Yingwen Liu, Yao Zhang, Sen Chen,Fu Song, Xiaofei Xie, Xiaohong Li and Lintan Sun. In Proc. of the 15th International Symposium on Theoretical Aspects of Software Engineering (TASE), 2021, 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. In Proc. of the 42st IEEE Symposium on Security and Privacy (Oakland, S&P), 2021, CCF-A [21]Patch Based Vulnerability Matching for Binary Programs. Yifei Xu, Zhengzi Xu, Bihuan Chen,Fu Song, Yang Liu and Ting Liu. In Proc. of the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA), 376–387, 2020, CCF-A [22]Quantitative Verification of Masked Arithmetic Programs Against Side-Channel Attacks. Pengfei Gao, Hongyi Xie, Jun Zhang,Fu Song*and Taolue Chen. In Proc. of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 155–173, 2019, CCF-B [23]SMT-Based Bounded Schedulability Analysis of the Clock Constraint Specification Language. Min Zhang,Fu Song*, Fei Gao, Frederic Mallet and Xiaohong Chen. In Proc. of the 22nd International Conference on Fundamental Approaches to Software Engineering (FASE), 61–78, 2019, CCF-B [24]Probabilistic Alternating-Time Mu-Calculus.Fu Song, Yedi Zhang, Yu Tang, Taolue Chen and Zhiwu Xu. In Proc. of the Thirty-Third AAAI Conference on Artificial Intelligence (AAAI), 6179–6186, 2019, CCF-A [25]Android Malware Family Classification and Characterization Using CFG and DFG. Zhiwu Xu, Kerong Ren andFu Song. In Proc. of the 13th International Symposium on Theoretical Aspects of Software Engineering (TASE), 2019, CCF-C [26]SCInfer: Refinement-based Verification of Software Countermeasures against Side-Channel Attacks. Jun Zhang, Pengfei Gao,Fu Song*and Chao Wang. In Proc. of the 30th International Conference on Computer Aided Verification (CAV),157–177,2018, CCF-A [27]Android Stack Machine. Taolue Chen, Jinlong He,Fu Song, Guozhen Wang, Zhilin Wu and Jun Yan (按姓排序).In Proc. The 30th International Conference on Computer Aided Verification (CAV), 487–504, 2018, CCF-A [28]KRust: A Formal Executable Semantics of Rust. Feng Wang,Fu Song*, Min Zhang, Xiaoran Zhu and Jun Zhang. In Proc. of the 12th International Symposium on Theoretical Aspects of Software Engineering (TASE), 44–51, 2018, CCF-C [29]Model Checking Pushdown Epistemic Game Structures. Taolue Chen,Fu Song*and Zhilin Wu (按姓排序). In Proc. of the 19th International Conference on Formal Engineering Methods (ICFEM), 36–53, 2017, CCF-C [30]Tractability of separation logic with inductive definitions: Beyond lists. Taolue Chen,Fu Songand Zhilin Wu (按姓排序). In Proc. of the 28th International Conference on Concurrency Theory (CONCUR), 37:1–37:17, 2017, CCF-B [31]SPAIN: Security Patch Analysis for Binaries - Towards Understanding the Pain and Pills. Zhengzi Xu, Bihuan Chen, Mahinthan Chandramohan, Yang Liu andFu Song. In Proc. of the 39th ACM/IEEE International Conference on Software Engineering (ICSE),462–472,2017, CCF-A [32]Reasoning about Periodicity on Infinite Words. Wanwei Liu,Fu Songand Ge Zhou. In Proc. of the 3rd Symposium on Dependable Software Engineering (SETTA), 200–215, 2017, CCF-C [33]Optimizing Backbone Filtering. Yueling Zhang, Jianwen Li, Min Zhang, Geguang Pu andFu Song. In Proc. of the 11th International Symposium on Theoretical Aspects of Software Engineering (TASE), 1–8, 2017, CCF-C [34]Verifying Pushdown Multi-Agent Systems against Strategy Logics. Taolue Chen,Fu Song, and Zhilin Wu (按姓排序). In Proc. of the 25th International Joint Conference on Artificial Intelligence (IJCAI), 180–186, 2016, CCF-A [35]Global Model Checking On Pushdown Multi-Agent Systems. Taolue Chen,Fu Song, and Zhilin Wu (按姓排序).In Proc. of the 30th AAAI Conference on Artificial Intelligence (AAAI), 2459–2465, 2016, CCF-A [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. In Proc. of the 26th International Conference on Concurrency Theory (CONCUR), 383–397, 2015, CCF-B [37]On the Satisfiability of Indexed Linear Temporal Logics. Taolue Chen,Fu Song, and Zhilin Wu (按姓排序). In Proc. of the 26th International Conference on Concurrency Theory (CONCUR), 254–267, 2015, CCF-B [38]Modeling and Verifying Google File System. Bo Li, Mengdi Wang, Yongxin Zhao, Geguang Pu, Huibiao Zhu, andFu Song. In Proc. of the 16th IEEE International Symposium on High Assurance Systems Engineering (HASE), 207–214, 2015 [39]Model-checking for Android Malware Detection.Fu Songand Tayssir Touili. In Proc. of the 12th Asian Symposium on Programming Languages and Systems (APLAS), 216–235, 2014, CCF-C [40]Extending Temporal Logics with Data Variable Quantifications.Fu Songand Zhilin Wu (按姓排序).In Proc. of the 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS), 253–265, 2014, CCF-C [41]LTL Model-Checking for Malware Detection.Fu Songand Tayssir Touili. In Proc. of the 19th International Conference on Tools and Algorithms for the Construction and Analysis ofSystems (TACAS), 416–431, 2013, CCF-B [42]Model Checking Dynamic Pushdown Networks.Fu Songand Tayssir Touili. In Proc. of the 11th Asian Symposium on Programming Languages and Systems (APLAS),33–49,2013, CCF-C [43]Model-checking Software Library API Usage Rules.Fu Songand Tayssir Touili.In Proc. of the 10th International Conference on Integrated Formal Methods (iFM), 192–207, 2013 [44]Pommade: Pushdown Model-Checking for Malware Detection.Fu Songand Tayssir Touili. In Proc. of the 9th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE), 607–610, 2013 [45]Efficient Malware Detection Using Model-Checking.Fu Songand Tayssir Touili. In Proc. of the 18th International Symposium on Formal Methods (FM), 418–433, 2012, CCF-B [46]Pumoc: A CTL Model-Checker for Sequential Programs.Fu Songand Tayssir Touili. In Proc. of the 27th IEEE/ACM International Conference on Automated Software Engineering (ASE), 346–349, 2012 [47]Pushdown Model Checking For Malware Detection.Fu Songand Tayssir Touili. In Proc. of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 110–125, 2012, CCF-B [48]Efficient CTL Model-Checking for Pushdown Systems.Fu Songand Tayssir Touili. In Proc. of the 22nd International Conference on Concurrency Theory (CONCUR), 434–449, 2011, CCF-B [49]A Distributed Clustering Algorithm for Voronoi Cell-Based Large Scale Wireless Sensor Network. Jiehui Chen, Chul soo Ki, andFu Song. In Proc. of the International Conference on Communications and Mobile Computing (CMC), 3:209–213, 2010 [50]Integrating the b-method into PVS. Jiaming Zhou, Jian Guo, andFu Song. In Proc. of the International Conference on Information Engineering and Computer Science (ICIECS), 1–4,2009 专利 [1]一种基于二元决策图的二值神经网络定量分析框架.宋富、张业迪，申请号202110619510.7 [2]一种基于样本鲁棒性差异的对抗样本检测方法.宋富、赵哲、陈光科，申请号202011284008.7 [3]一种基于攻击成本的对抗样本检测方法.宋富、赵哲、陈光科，申请号202011285900.7 [4]一种基于图同构的程序高阶功耗侧信道安全性的证明方法.宋富、高鹏飞、谢弘毅，申请号CN202010913876.0 [5]一种基于GPU的模型计数及其约束的求解方法.宋富、高鹏飞、谢弘毅，申请号CN202010908484.5 [6]一种基于分治的程序高阶功耗侧信道安全性的证明方法.宋富、高鹏飞、谢弘毅，申请号CN202010908485.X [7]一种抗功耗侧信道攻击对策验证方法.宋富，专利号ZL 2018 1 0626315.5，授权公告日2021年10月26日 [8]基于语音声学特征压缩的语音对抗样本防御方法及应用.宋富、陈光科、赵哲，申请号202111060044.X |
