• 模型检查
• 系统分析与验证
• 计算机安全
• 人工智能安全

招收硕士、博士

081202-计算机软件与理论
083500-软件工程
083900-网络空间安全

形式化验证
程序分析
网络空间安全

2009-12--2013-04   巴黎狄德罗大学（巴黎七大）   博士
2007-03--2009-06   华东师范大学   硕士
2002-09--2006-06   宁波大学   学士

2023-09~现在, 中国科学院软件研究所, 研究员
2021-08~2023-09,上海科技大学, 副教授、研究员
2016-08~2021-07,上海科技大学, 助理教授、研究员
2016-01~2016-07,华东师范大学, 副研究员
2013-08~2015-12,华东师范大学, 讲师

2024-01-01-今,中国计算机学会形式化方法专业委员会常委, 形式化方法专业组委员

编译原理
计算理论
信息安全研究方法
嵌入式系统开发实践

   

（1） 中国电子学会2023网络空间安全优秀论文, 其他, 2023
（2） 中国计算机学会形式化方法专业委员会2023年度博士学位论文激励计划, 一等奖, 其他, 2023
（3） 亚马逊研究奖, 其他, 2022

（ 1 ） 基于语音声学特征压缩的语音对抗样本防御方法及应用, 发明专利, 2022, 第 1 作者, 专利号: CN114242083A

（ 2 ） 基于二元决策图的二值神经网络定量分析方法, 发明专利, 2021, 第 1 作者, 专利号: CN113378009A

（ 3 ） 超导抗旁路攻击加密装置及加密方法, 发明专利, 2021, 第 3 作者, 专利号: 202110178609.8

（ 4 ） 一种基于攻击成本的对抗样本检测方法, 发明专利, 2021, 第 1 作者, 专利号: CN112381152A

（ 5 ） 一种基于样本鲁棒性差异的对抗样本检测方法, 发明专利, 2021, 第 1 作者, 专利号: CN112381150A

（ 6 ） 一种基于图同构的程序高阶功耗侧信道安全性的证明方法, 发明专利, 2021, 第 1 作者, 专利号: CN112364392A

（ 7 ） 一种基于GPU的模型计数及其约束的求解方法, 发明专利, 2020, 第 1 作者, 专利号: CN112131583A

（ 8 ） 一种基于分治的程序高阶功耗侧信道安全性的证明方法, 发明专利, 2020, 第 1 作者, 专利号: CN112134729A

（ 9 ） 一种抗功耗侧信道攻击对策验证方法, 发明专利, 2018, 第 1 作者, 专利号: CN108809622A

   

[1] Luwei Cai, 宋富, Taolue Chen. Towards Efficient Verification of Constant-Time Cryptographic Implementations. Proceedings of the ACM on Software Engineering (FSE)[J]. 2024, 第 2 作者  通讯作者  
[2] Zichen Wang, Jingyi Wang, 宋富, Kun Wang, Hongyi Pu, Peng Cheng. K-RAPID: A Formal Executable Semantics of the RAPID Robot Programming Language. 10th ACM Cyber-Physical System Security Workshop (CPSS). 2024, 第 3 作者
[3] Jiaxiang Liu, Yunhan Xing, 施晓牧, 宋富, zhiwu xu, Ming Zhong. Abstraction and Refinement: Towards Scalable and Exact Verification of Neural Networks. ACM Transactions on Software Engineering and Methodology (TOSEM)[J]. 2024, 第 4 作者
[4] Pu Sun, 宋富, Yuqi Chen, Taolue Chen. EasyBC: A Cryptography-Specific Language for Security Analysis of Block Ciphers against Differential Cryptanalysis. Proceedings of the ACM on Programming Languages (POPL)[J]. 2024, 第 2 作者  通讯作者  
[5] gao pengfei, 宋富, Taolue Chen. Compositional Verification of First-Order Masking Countermeasures against Power Side-Channel Attacks. ACM Transactions on Software Engineering and Methodology (TOSEM)[J]. 2024, 第 2 作者  通讯作者  
[6] Guangke Chen, Yedi Zhang, 宋富. SLMIA-SR: Speaker-Level Membership Inference Attacks against Speaker Recognition Systems. 31st Annual Network and Distributed System Security Symposium (NDSS). 2024, 第 3 作者  通讯作者  
[7] Zhensu Sun, Xiaoning Du, 宋富, Shangwen Wang, Li Li. When Neural Code Completion Models Size up the Situation: Attaining Cheaper and Faster Completion through Dynamic Model Inference. 45th IEEE/ACM International Conference on Software Engineering (ICSE). 2024, 第 3 作者
[8] Zhe Zhao, Guangke Chen, Tong Liu, Taishan Li, 宋富, Jingyi Wang, Jun Sun. Attack as Detection: Using Adversarial Attack Methods to Detect Abnormal Examples. ACM Transactions on Software Engineering and Methodology (TOSEM)[J]. 2024, 第 5 作者  通讯作者  
[9] Zhang, Yedi, Zhao, Zhe, Chen, Guangke, Song, Fu, Chen, Taolue. Precise Quantitative Analysis of Binarized Neural Networks: A BDD-based Approach. ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY[J]. 2023, 32(3): http://dx.doi.org/10.1145/3563212.
[10] 宋富. 密码实现安全形式化验证发展现状与展望. 前瞻科技. 2023, 第 1 作者2(1): 90-105, http://lib.cqvip.com/Qikan/Article/Detail?id=7109340611.
[11] Sun, Pu, Chen, Sen, Fan, Lingling, Gao, Pengfei, Song, Fu, Yang, Min. VenomAttack: automated and adaptive activity hijacking in Android. FRONTIERS OF COMPUTER SCIENCE[J]. 2023, 17(1): 187-204, 
[12] Yedi Zhang, 宋富, Jun Sun. QEBVerif: Quantization Error Bound Verification of Neural Networks. 35th International Conference on Computer Aided Verification (CAV). 2023, 第 2 作者  通讯作者  
[13] Zhen Liang, 刘万伟, 宋富, Bai Xue, Wenjing Yang, Ji Wang, Zhengbin Pang. Qualitative and Quantitative Model Checking against Recurrent Neural Networks. Journal of Computer Science and Technology[J]. 2023, 第 3 作者
[14] Zhensu Sun, Xiaoning Du, 宋富, Li Li. CodeMark: Imperceptible Watermarking for Code Datasets against Neural Code Completion Models. 31th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE). 2023, 第 3 作者  通讯作者  
[15] Mingyang Liu, 宋富, Taolue Chen. Automated Verification of Correctness for Masked Arithmetic Programs. 35th International Conference on Computer Aided Verification (CAV). 2023, 第 2 作者  通讯作者  
[16] Zhensu Sun, Xiaoning Du, 宋富, Shangwen Wang, Mingze Ni, Li Li. Don’t Complete It! Preventing Unhelpful Code Completion for Productive and Sustainable Neural Code Completion Systems. 44th IEEE/ACM International Conference on Software Engineering (ICSE). 2023, 第 3 作者
[17] Chen, Guangke, Zhao, Zhe, Song, Fu, Chen, Sen, Fan, Lingling, Wang, Feng, Wang, Jiashui. Towards Understanding and Mitigating Audio Adversarial Examples for Speaker Recognition. IEEE TRANSACTIONS ON DEPENDABLE AND SECURE COMPUTING[J]. 2023, http://arxiv.org/abs/2206.03393.
[18] Guangke Chen, Yedi Zhang, Zhe Zhao, 宋富. QFA2SR: Query-Free Adversarial Transfer Attacks to Speaker Recognition Systems. 32nd USENIX Security Symposium (Security). 2023, 第 4 作者  通讯作者  
[19] Chen, Guangke, Zhao, Zhe, Fu Song, Chen, Sen, Fan, Lingling, Liu, Yang. AS2T: Arbitrary Source-To-Target Adversarial Attack on Speaker Recognition Systems. IEEE TRANSACTIONS ON DEPENDABLE AND SECURE COMPUTING[J]. 2023, http://arxiv.org/abs/2206.03351.
[20] Ye Tao, Wanwei Liu, 宋富, Zhen Liang, Ji Wang, Hongxu Zhu. An Automata-Theoretic Approach to Synthesizing Binarized Neural Networks. 21st International Symposium on Automated Technology for Verification and Analysis (ATVA). 2023, 第 3 作者
[21] Gao pengfei, Yedi Zhang, 宋富, Taolue Chen, Francois-Xavier Standaert. Compositional Verification of Efficient Masking Countermeasures against Side-Channel Attacks. Proceedings of the ACM on Programming Languages (OOPSLA)[J]. 2023, 第 3 作者  通讯作者  
[22] Limin Wang, Lei Bu, 宋富. SCAGuard: Detection and Classification of Cache Side-Channel Attacks via Attack Behavior Modeling and Similarity Comparison. 60th ACM/IEEE Design Automation Conference (DAC). 2023, 第 3 作者
[23] 杨珉, 张超, 宋富, 张源. 系统软件安全专题前言. 软件学报[J]. 2022, 第 3 作者33(6): 1959-1960, http://lib.cqvip.com/Qikan/Article/Detail?id=7107361356.
[24] Gao, Pengfei, Xu, Yongjie, Song, Fu, Chen, Taolue. Model-based automated testing of JavaScript Web applications via longer test sequences. 中国计算机科学前沿:英文版[J]. 2022, 16(3): 53-66, http://lib.cqvip.com/Qikan/Article/Detail?id=7107388008.
[25] Yuxin Fan, Fu Song, Taolue Chen, Liangfeng Zhang, Wanwei Liu. PoS4MPC: Automated Security Policy Synthesis for Secure Multi-party Computation. 34rd International Conference on Computer Aided Verification (CAV). 2022, 385-406, http://dx.doi.org/10.1007/978-3-031-13185-1_19.
[26] Yedi Zhang, Zhe Zhao, Guangke Chen, 宋富, Min Zhang, Taolue Chen. QVIP: An ILP-based Formal Verification Approach for Quantized Neural Networks. 37th IEEE/ACM International Conference on Automated Software Engineering (ASE). 2022, 第 4 作者  通讯作者  
[27] Limin Wang, Lei Bu, 宋富. Locality based Cache Side Channel Attack Detection. 10th International Workshop on Security Proofs for Embedded Systems (PROOFS). 2022, 第 3 作者
[28] Bu, Lei, Zhao, Zhe, Duan, Yuchao, Fu Song. Taking Care of the Discretization Problem: A Comprehensive Study of the Discretization Problem and a Black-Box Adversarial Attack in Discrete Integer Domain. IEEE TRANSACTIONS ON DEPENDABLE AND SECURE COMPUTING[J]. 2022, 19(5): 3200-3217, http://dx.doi.org/10.1109/TDSC.2021.3088661.
[29] Gao Pengfei, Xie Hongyi, Pu Sun, Jun Zhang, Fu Song, Chen, Taolue. Formal Verification of Masking Countermeasures for Arithmetic Programs. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING[J]. 2022, 48(3): 973-1000, http://dx.doi.org/10.1109/TSE.2020.3008852.
[30] Xu, Yongjie, Fu Song, Chen, Taolue. ESampler: Boosting sampling of satisfying assignments for Boolean formulas via derivation. JOURNAL OF SYSTEMS ARCHITECTURE[J]. 2022, 129: http://dx.doi.org/10.1016/j.sysarc.2022.102615.
[31] Zhe Zhao, Yedi Zhang, Guangke Chen, 宋富, Taolue Chen, Jiaxiang Liu. CLEVEREST: Accelerating CEGAR-based Neural Network Verification via Adversarial Attacks. 29th Static Analysis Symposium (SAS). 2022, 第 4 作者  通讯作者  
[32] Qi Qin, JulianAndres JiYang, 宋富, Taolue Chen, Xinyu Xing. DeJITLeak: Eliminating JIT-Induced Timing Side-Channel Leaks. 21st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE). 2022, 第 3 作者  通讯作者  
[33] Sun, Zhensu, Du, Xiaoning, Fu Song, Ni, Mingze, Li, Li. CoProtector: Protect Open-Source Code against Unauthorized Training Usage with Data Poisoning. Proceedings of The Web Conference (WWW). 2022, 
[34] 杨珉, 张超, 宋富, 张源. Preface to Special Issue on System Software Security. International Journal of Software and Informatics[J]. 2022, 第 3 作者
[35] Gao, Pengfei, Xie, Hongyi, Fu Song, Chen, Taolue. A Hybrid Approach to Formal Verification of Higher-Order Masked Arithmetic Programs. ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY[J]. 2021, 30(3): http://dx.doi.org/10.1145/3428015.
[36] Sen Chen, Lingling Fan, 宋富, Cuiyun Gao, Yang Liu. Peeking into the Gray Area of Mobile World: Empirical Investigation of Unlabeled Android Apps in Industry. 32th International Symposium on Software Reliability Engineering (ISSRE). 2021, 第 3 作者
[37] Lin, Yingwen, Zhang, Yao, Chen, Sen, Song, Fu, Xie, Xiaofei, Li, Xiaohong, Sun, Lintan, IEEE COMP SOC. Inferring Loop Invariants for Multi-Path Loops. 2021 INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING (TASE 2021). 2021, 63-70, 
[38] Xingwu Guo, Wenjie Wan, Zhaodi Zhang, Min Zhang, Fu Song, Xuejun Wen. Eager Falsification For Accelerating Robustness Verification of Deep Neural Networks. 32th International Symposium on Software Reliability Engineering (ISSRE). 2021, 
[39] Chen Guangke, Chen Sen, Fan Lingling, Du Xiaoning, Zhao Zhe, Song Fu, Liu Yang. Who is Real Bob? Adversarial Attacks on Speaker Recognition Systems. 42st IEEE Symposium on Security and Privacy (S&P). 2021, http://arxiv.org/abs/1911.01840.
[40] Fu Song, Lei, Yusi, Chen, Sen, Fan, Lingling, Liu, Yang. Advanced evasion attacks and mitigations on practical ML-based phishing website classifiers. INTERNATIONAL JOURNAL OF INTELLIGENT SYSTEMS[J]. 2021, 36(9): 5210-5240, http://dx.doi.org/10.1002/int.22510.
[41] Yongjie Xu, 宋富, Taolue Chen. ESAMPLER: Efficient Sampling of Satisfying Assignments for Boolean Formulas. 7th Symposium on Dependable Software Engineering Theories, Tools and Applications (SETTA). 2021, 第 2 作者  通讯作者  
[42] Zhang, Yedi, Zhao, Zhe, Chen, Guangke, Fu Song, Chen, Taolue. BDD4BNN: A BDD-based Quantitative Analysis Framework for Binarized Neural Networks. 33rd International Conference on Computer Aided Verification (CAV). 2021, http://arxiv.org/abs/2103.07224.
[43] Zhao, Zhe, Chen, Guangke, Wang, Jingyi, Yang, Yiwei, Fu Song, Sun, Jun. Attack as Defense: Characterizing Adversarial Examples using Robustness. 30th ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA). 2021, http://arxiv.org/abs/2103.07633.
[44] Liu, WanWei, Song, Fu, Zhang, TangHaoRan, Wang, Ji. Verifying ReLU Neural Networks from a Model Checking Perspective. JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY[J]. 2020, 35(6): 1365-1381, http://lib.cqvip.com/Qikan/Article/Detail?id=7103652900.
[45] Yifei Xu, Xu, Zhengzi, 陈碧欢, Fu Song, Yang Liu, Ting Liu. Patch Based Vulnerability Matching for Binary Programs. 9th ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA). 2020, 
[46] Gao, Pengfei, Zhang, Jun, Fu Song, Wang, Chao. Verifying and Quantifying Side-channel Resistance of Masked Software Implementations. ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY[J]. 2019, 28(3): http://dx.doi.org/10.1145/3330392.
[47] Xu, Zhiwu, Ren, Kerong, Song, Fu. Android Malware Family Classification and Characterization Using CFG and DFG. 2019 13TH INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING (TASE 2019)[J]. 2019, 49-56, http://dx.doi.org/10.1109/TASE.2019.00014.
[48] Pengfei Gao, Hongyi Xie, Jun Zhang, Fu Song, Taolue Chen. Quantitative Verification of Masked Arithmetic Programs against Side-Channel Attacks. International Conference on Tools and Algorithms for the Construction and Analysis of Systems[J]. 2019, 
[49] Pan, Haiyu, Song, Fu, Cao, Yongzhi, Qian, Junyan. Fuzzy Pushdown Termination Games. IEEE TRANSACTIONS ON FUZZY SYSTEMS[J]. 2019, 27(4): 760-774, 
[50] Min Zhang, Fu Song, Fei Gao, Mallet, Frederic, Xiaohong Chen. SMT-Based Bounded Schedulability Analysis of the Clock Constraint Specification Language. International Conference on Theoretical Aspects of Software Engineering. 2019, 
[51] Zhang, Yedi, Song, Fu, Chew, Taolue. Making Agents' Abilities Explicit. IEEE ACCESS[J]. 2019, 7: 101804-101819, http://dx.doi.org/10.1109/ACCESS.2019.2931514.
[52] Zhiwu Xu, Fu Song, Kerong Ren. Android Malware Family Classification and Characterization Using CFG and DFG. International Symposium on Theoretical Aspects of Software Engineering. 2019, 
[53] Fu Song, Zhang, Yedi, Chen, Taolue, Tang, Yu, Xu, Zhiwu. Probabilistic Alternating-Time mu-Calculus. THIRTY-THIRD AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE / THIRTY-FIRST INNOVATIVE APPLICATIONS OF ARTIFICIAL INTELLIGENCE CONFERENCE / NINTH AAAI SYMPOSIUM ON EDUCATIONAL ADVANCES IN ARTIFICIAL INTELLIGENCE[J]. 2019, 6179-6186, http://apps.webofknowledge.com/CitedFullRecord.do?product=UA&colName=WOS&SID=5CCFccWmJJRAuMzNPjj&search_mode=CitedFullRecord&isickref=WOS:000486572500087.
[54] Zhang, Min, Song, Fu, Mallet, Frederic, Chen, Xiaohong, Hahnle, R, VanderAalst, W. SMT-Based Bounded Schedulability Analysis of the Clock Constraint Specification Language. FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING (FASE 2019)[J]. 2019, 11424: 61-78, 
[55] Wang Feng, Song Fu, Zhang Min, Zhu Xiaoran, Zhang Jun. KRust: A Formal Executable Semantics of Rust. PROCEEDINGS 2018 12TH INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING (TASE 2018)[J]. 2018, 44-51, http://dx.doi.org/10.1109/TASE.2018.00014.
[56] Song, Fu. Analyzing pushdown systems with stack manipulation. INFORMATION AND COMPUTATION[J]. 2018, 259: 41-71, http://dx.doi.org/10.1016/j.ic.2017.12.003.
[57] Zhang Jun, Gao Pengfei, Song Fu, Wang Chao. SCINFER: Refinement-Based Verification of Software Countermeasures Against Side-Channel Attacks. COMPUTER AIDED VERIFICATION, CAV 2018, PT II[J]. 2018, 10982: 157-177, 
[58] Chen Taolue, He Jinlong, Song Fu, Wang Guozhen, Wu Zhilin, Yan Jun. Android Stack Machine. COMPUTER AIDED VERIFICATION, CAV 2018, PT II. 2018, 10982: 487-504, 
[59] Zhang, Yueling, Zhang, Min, Pu, Geguang, Song, Fu, Li, Jianwen. Towards backbone computing: A Greedy-Whitening based approach. AI COMMUNICATIONS[J]. 2018, 31(3): 267-280, https://www.webofscience.com/wos/woscc/full-record/WOS:000432544800004.
[60] 张业迪, 宋富. 异构多智能体系统模型检查. 软件学报[J]. 2018, 第 2 作者29(6): 1582-1594, http://lib.cqvip.com/Qikan/Article/Detail?id=675408083.
[61] Lei, Yusi, Song, Fu, Liu, Wanwei, Zhang, Min. On the complexity of omega-pushdown automata. SCIENCE CHINA-INFORMATION SCIENCES[J]. 2017, 60(11): https://www.webofscience.com/wos/woscc/full-record/WOS:000417334600008.
[62] Zhang, Yueling, Li, Jianwen, Zhang, Min, Pu, Geguang, Song, Fu. Optimizing Backbone Filtering. PROCEEDINGS 11TH 2017 INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING (TASE). 2017, 39-46, http://apps.webofknowledge.com/CitedFullRecord.do?product=UA&colName=WOS&SID=5CCFccWmJJRAuMzNPjj&search_mode=CitedFullRecord&isickref=WOS:000426968400006.
[63] Yusi LEI, Fu SONG, Wanwei LIU, Min ZHANG. On the complexity of ω-pushdown automata. 中国科学：信息科学（英文版）[J]. 2017, 60(11): 152-166, http://lib.cqvip.com/Qikan/Article/Detail?id=673606479.
[64] Chen Taolue, Song Fu, Wu Zhilin. Model Checking Pushdown Epistemic Game Structures. FORMAL METHODS AND SOFTWARE ENGINEERING, ICFEM 2017[J]. 2017, 10610: 36-53, 
[65] 刘万伟, Fu Song, Ge Zhou. Reasoning about Periodicity on Infinite Words. Symposium on Dependable Software Engineering (SETTA)[J]. 2017, 
[66] Xu, Zhengzi, Chen, Bihuan, Chandramohan, Mahinthan, Liu, Yang, Song, Fu. SPAIN: Security Patch Analysis for Binaries Towards Understanding the Pain and Pills. 2017 IEEE/ACM 39TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING (ICSE). 2017, 462-472, 
[67] Taolue Chen, Fu Song, Zhilin Wu. Tractability of separation logic with inductive definitions: Beyond lists. International Conference on Concurrency Theory (CONCUR)[J]. 2017, 
[68] Chen Taolue, Song Fu, Wu Zhilin, Bowen JP, Liu Z, Zhang Z. Formal Reasoning on Infinite Data Values: An Ongoing Quest. ENGINEERING TRUSTWORTHY SOFTWARE SYSTEMS (SETSS 2016). 2017, 10215: 195-257, 
[69] Taolue Chen, Fu Song, 吴志林. Verifying pushdown multi-agent systems against strategy logics. International Joint Conference on Artificial Intelligence (IJCAI 2016)[J]. 2016, 
[70] Song, Fu, Wu, Zhilin. On temporal logics with data variable quantifications: Decidability and complexity. INFORMATION AND COMPUTATION[J]. 2016, 251: 104-139, http://dx.doi.org/10.1016/j.ic.2016.08.002.
[71] Chen Taolue, Song Fu, Wu Zhilin. Global Model Checking on Pushdown Multi-Agent Systems. THIRTIETH AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE. 2016, 2459-2465, http://apps.webofknowledge.com/CitedFullRecord.do?product=UA&colName=WOS&SID=5CCFccWmJJRAuMzNPjj&search_mode=CitedFullRecord&isickref=WOS:000485474202070.
[72] Fu Song. Survey on Formal Models to Reason about Infinite Data Values. Journal of Software. 2016, 
[73] Song, Fu, Touili, Tayssir. Model-checking software library API usage rules. SOFTWAREANDSYSTEMSMODELING[J]. 2016, 15(4): 961-985, https://www.webofscience.com/wos/woscc/full-record/WOS:000384535800004.
[74] 宋富, 吴志林. 面向无穷数据的形式模型综述. 软件学报[J]. 2016, 第 1 作者682-690, http://lib.cqvip.com/Qikan/Article/Detail?id=668151132.
[75] Fu Song, 缪炜恺, 蒲戈光, Min Zhang. On reachability analysis of pushdown systems with transductions: Application to boolean programs with call-by-reference. the 26th International Conference on Concurrency Theory[J]. 2015, 
[76] Taolue Chen, 宋富, 吴志林. On the Satisfiability of Indexed Linear Temporal Logics. 26th International Conference on Concurrency Theory (CONCUR 2015)[J]. 2015, 第 2 作者
[77] Song, Fu, Touili, Tayssir. Model checking dynamic pushdown networks. FORMAL ASPECTS OF COMPUTING[J]. 2015, 27(2): 397-421, http://dx.doi.org/10.1007/s00165-014-0330-y.
[78] Fu Song. Model-checking for android malware detection. the 12th Asian Symposium on Programming Languages and Systems. 2014, 
[79] 吴志林. Extending Temporal Logics with Data Variable Quantifications. 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). 2014, 
[80] Song, Fu, Touili, Tayssir. Efficient CTL model-checking for pushdown systems. THEORETICAL COMPUTER SCIENCE[J]. 2014, 549: 127-145, http://dx.doi.org/10.1016/j.tcs.2014.07.001.
[81] Song, Fu, Touili, Tayssir. Pushdown model checking for malware detection. INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER[J]. 2014, 16(2): 147-173, https://www.webofscience.com/wos/woscc/full-record/WOS:000209673000003.
[82] Song Fu, Touili Tayssir, Piterman N, Smolka SA. LTL Model-Checking for Malware Detection. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2013. 2013, 7795: 416-431, 
[83] Fu Song. Pommade: pushdown model-checking for malware detection. the 9th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering. 2013, 
[84] Fu Song. Efficient malware detection using model-checking. the 18th International Symposium on Formal Methods. 2012, 
[85] Song Fu, Touili Tayssir, IEEE. PuMoC: A CTL Model-Checker for Sequential Programs. 2012 PROCEEDINGS OF THE 27TH IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING (ASE). 2012, 346-349, 
[86] Song Fu, Touili Tayssir, Flanagan C, Konig B. Pushdown Model Checking for Malware Detection. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2012. 2012, 7214: 110-125, 
[87] Song, Fu, Touili, Tayssir. Efficient CTL Model-Checking for Pushdown Systems. CONCUR 2011: CONCURRENCY THEORY[J]. 2011, 6901: 434-+, 

   

（ 1 ） 恶意软件静态分析与检测关键技术研究, 负责人, 国家任务, 2015-01--2017-12
（ 2 ） 二进制程序的模型检查技术研究, 负责人, 地方任务, 2015-01--2016-12
（ 3 ） 复杂二进制程序静态分析及其应用研究, 负责人, 地方任务, 2014-07--2016-06
（ 4 ） 大规模概率并发实时系统模型检验, 参与, 国家任务, 2016-01--2020-12
（ 5 ） 不确定环境下可信国产城轨控制系统（iCMTCt）构造关键技术研究, 参与, 国家任务, 2015-01--2016-12
（ 6 ） 车载网和车载云中信息安全与隐私保护关键技术研究, 参与, 国家任务, 2016-01--2019-12
（ 7 ） 汽车电子功能安全体系设计及功能安全模型及验证工具开发, 参与, 国家任务, 2014-01--2016-11
（ 8 ） 交互式应用异常分析方法和技术, 参与, 国家任务, 2018-01--2020-12
（ 9 ） 掩码程序安全实现的关键技术研究, 负责人, 国家任务, 2021-01--2024-12
（ 10 ） 2023年度所杰青项目, 负责人, 研究所自主部署, 2023-12--2027-12
（ 11 ） 开放环境下的智能算法泛化性研究, 参与, 研究所自主部署, 2023-12--2028-11
（ 12 ） 面向大规模二进制程序的软件成分分析, 参与, 研究所自主部署, 2023-07--2024-12

（1）Verifying Pushdown Multi-Agent Systems against Strategy Logics   2016-07-09
（2）On reachability analysis of pushdown systems with transductions: Application to boolean programs with call-by-reference   2015-09-01

详见 https://songfu1983.github.io/