Publications

Books and Book Articles

  1. 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. 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. Accepted, 2019. (SCI, EI, CCF-A)
  2. 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, IF=8.415)
  3. Analyzing Pushdown Systems with Stack Manipulation. Fu Song. Information and Computation, volume 259(1), pages 41-71, 2018. (SCI,EI,CCF-A)
  4. 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)
  5. Model-Checking for Heterogeneous Multi-agent Systems (In Chinese). Yedi Zhang and Fu Song. Journal of Software (JOS), volume 29(6), 2018. (EI)
  6. 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-B)
  7. 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)
  8. Model-checking software library API usage rules. Fu Song and Tayssir Touili. Journal on Software and Systems Modeling(SoSym), volume 15(4), pages 961-985, 2016 (SCI,EI,CCF-B)
  9. 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 (IJNS), volume 18(6), pages 1143-1151, November 2016. (EI)
  10. Survey on Formal Models to Reason about Infinite Data Values (In Chinese). Fu Song and Zhilin Wu. Journal of Software (JOS), Volume 27(3):a14, March 2016. (EI)
  11. Model Checking Dynamic Pushdown Networks. Journal on Formal Aspects of Computing (FAOC), volume 27(2), Pages 397-421, March 2015. Fu Song and Tayssir Touili. (SCI,EI,CCF-B)
  12. Efficient CTL Model-Checking for Pushdown Systems. Fu Song and Tayssir Touili. Journal on Theoretical Computer Science (TCS), Volume 549, Pages 127-145, September 2014. (SCI,EI,CCF-B)
  13. Pushdown Model-Checking for Malware Detection. Fu Song and Tayssir Touili. Journal on Software Tools for Technology Transfer (STTT), Volume 16(2), Pages 147-173, April 2014. (EI,CCF-C)

Refereed Conference and Workshop Articles

  1. A Hybrid Approach to Formal Verification of Higher-Order Masked Arithmetic Programs. Pengfei Gao, Hongyi Xie, Fu Song* and Taolue Chen. To Submit, 2019.
  2. A Systematic Study on the Threat of Phishing Website Classifiers: Advanced Evasion Attacks and Mitigations. Yusi Lei, Sen Chen, Lingling Fan, Fu Song and Yang Liu. To Submit, 2019.
  3. Things You May Not Know About Adversarial Example: A Black-box Adversarial Image Attack. Yuchao Duan, Zhe Zhao, Lei Bu and Fu Song. To Submit, 2019.
  4. Making Strategic Abilities Explicit. Yedi Zhang, Fu Song and Taolue Chen. To Submit, 2019.
  5. 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)
  6. 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), 2019. (EI, CCF-B)
  7. 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), 2019. (EI, CCF-B)
  8. 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), 2019. (CCF-A)
  9. 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)
  10. 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)
  11. Android Stack Systems. [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)
  12. 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)
  13. 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)
  14. 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)
  15. 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)
  16. 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)
  17. 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)
  18. 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)
  19. 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)
  20. 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)
  21. 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)
  22. 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)
  23. 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)
  24. 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)
  25. 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 2013). Russia. August 18-26, 2013. (EI)
  26. 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)
  27. 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)
  28. 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)
  29. 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-B)
  30. 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)
  31. 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)
  32. 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)
  33. 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)