English
分享到
师资队伍
photo
姓名: 周旻
职称: 副研究员
电子邮件: mzhou@tsinghua.edu.cn
工作地点: 清华大学东配楼11区307室
电话: 010-62773275
研究领域: 代码静态分析、软件工程、形式化方法、软件测试等

教育背景

2007.7-2014.1     工学博士,清华大学计算机科学与技术系,计算机科学与技术专业

2003.8-2007.7    理学学士,清华大学数学科学系,数学与应用数学专业

科研经历

2019.11-至今         清华大学软件学院副研究员,研究方向:软件分析验证、软件工程

2016.1-2019.11      清华大学软件学院助理研究员,研究方向:软件分析验证、软件工程

2014.1-2016.1       清华大学软件学院博士后,研究方向:形式化方法、软件工程

2011.6-2011.8       法国Verimag实验室研究实习生

研究兴趣

代码静态分析、软件工程、形式化方法、软件测试等

个人简介

周旻博士本科毕业于清华大学数学系,博士阶段重点研究软件理论与形式化技术,在该领域深耕多年。共在高水平国际期刊与会议上发表学术论文38篇,其中近5年发表论文23篇(SCI期刊8篇、EI会议15篇;CCF A类10篇、B类1篇、C类8篇)。根据CCF发布的推荐国际学术会议和期刊目录,本人发表的论文中包括TSE(IEEE Transactions on Software Engineering)、TIE(IEEE Transactions on Industrial Engineering)、TEC(IEEE Transactions on Evolutionary Computation)、TC(IEEE Transactions on Computers)、AI(Artificial Intelligence)、JAR(Journal of Automated Reasoning)等软件工程、人工智能、计算机理论等顶级期刊,以及CAV、ASE、ICSE、ISSTA等形式化方法、软件工程领域顶级会议。发表的论文中包含多篇高影响因子论文,例如:IEEE Transactions on Industrial Electronics(IF>8.2)、IEEE Transactions on Evolutionary Computation(IF>11.5)等。

代表性学术贡献和学术成果影响力方面。2010年,本人在CAV会议发表的论文“On Array Theory of Bounded Elements”是该会议举办以来,大陆学者首次发表的长文,属于突破性成果。CAV是形式化领域的顶级会议(CCF A类),行业认可度很高。该论文提出了一种新的数组理论域,能够对程序分析验证中的路径条件判定问题提供理论支撑。2013年发表的论文“Component-based Modeling and Code Synthesis for Cyclic Programs”获得COMPSAC 2013国际学术会议最佳论文,该论文提出了一种针对周期执行程序的模型驱动开发方式,给出了全生命周期中建模、分析、验证、代码生成等技术方案。2016年的论文“Automatic Fix for C Integer Errors by Precision Improvement”首次提出了一种基于精度提升程序缺陷自动修复方法,并获得了COMPSAC2016的最佳论文。2017年,面向航空发动机控制程序,提出了一种针对单调速率调度程序的验证方法,并首次在代码实现层面对单调速率调度算法的代码实现进行了验证,相关论文发表于TIE。针对自动定理证明的核心技术——可满足性模理论(SMT),本人对其并行化求解问题开展了深入研究,并形成了原型工具,2018年在Artificial Intelligence上发表了论文“Parallelizing SMT solving: Lazy decomposition and conciliation”。关于整数缺陷修复的两个研究工作,分别于2018、2019年发表在了Transactions on Computers和Transactions on Dependable and Secure Computing上,是早期缺陷自动修复领域的重要研究工作。

科研项目方面,积极参与国家重大科研项目。主持了博士后基金(优秀10万,项目负责人)、国家自然科学基金青年基金(26万,项目负责人)、北京市科委项目(98万,子课题负责人)、科技部重点研发项目(64万,子课题负责人)。本人主持了多项企事业单位委托课题,委托单位覆盖了:中国科学院信息工程研究所、中国航发控制系统研究所、中央国债登记结算有限责任公司、中车青岛四方车辆研究所有限公司,等等。近5年主持项目经费超过1400万元。此外,还作为项目骨干积极参与了多项国家级科研项目,包括:某973项目(专题负责人)、科技部重点研发项目(骨干)、自然科学基金重大项目(骨干)等等。

科研成果转化方面,基于理论研究成果,主持研发了具有完全自主知识产权的Tsmart代码静态分析工具,具有优秀的功能、性能。工具参加NASAC(2018年)的“源代码漏洞检测原型工具”竞赛,并荣获一等奖。工具获得了CWE-Compatibility认证。工具已经在多个重要行业应用:(1)国产操作系统评估:成功检测到13条被确认的代码缺陷,提交6份内核缺陷分析报告,加速了国产操作系统自主可控进程;(2)航发控制系统分析验证:部署于中国航发控制系统研究所,在生产环境中对多款发动机控制代码检测;(3)轨道交通嵌入式系统代码分析:在中国中车节能自动驾驶项目中检测到300多个内存安全等问题;(4)卫星遥感算法测评:构建业务算法分析和评估平台,并协助举办相关比赛;(5)金融安全领域:在中央国债登记结算有限公司8个项目上实现应用,范围涵盖中债信息网、理财信披、估值创新二期等3个业务条线,总共检测到6类典型的潜在高危漏洞和3类严重代码BUG,共计243个;(6)除此之外,工具还在Linux、OpenSSL等十余个重要开源项目中检测到代码缺陷70余,且大部分已被官方确认并修复。工具拥有多项应用证明,获得了业界认可。

代表性论著

  1. Chi Li, Min Zhou, Xinrong Han, Ming Gu. Sensing Error Handling Bugs in SSL Library Usages. TrustCom 2021. [EI收录,CCF C]

  2. Chi Li, Yuexing Wang, Min Zhou, Ming Gu. Scalable Fault Detection Based on Precise Access Path. APSEC 2021. [EI收录,CCF C]

  3. Xi Cheng, Min Zhou, Xiaoyu Song, Ming Gu, Jiaguang Sun. Automatic Integer Error Repair by Proper-Type Inference. IEEE Transactions on Dependable and Secure Computing. 2021, 18(2): 918~935. [SCI收录,CCF A]

  4. Yuexing Wang, Guang Chen, Min Zhou, Ming Gu, Jiaguang Sun. TsmartGP: A Tool for Finding Memory Defects with Pointer Analysis. ASE 2019. [EI收录,CCF A]

  5. Chi Li, Min Zhou, Zuxing Gu, Ming Gu, Hongyu Zhang. Ares: Inferring Error Specifications through Static Analysis. In Proceedings of the 34th IEEE/ACM International Conference on Automated Software Engineering (ASE), pp. 1174-1177, 11-15 Nov. 2019. [EI收录,CCF A]

  6. Chi Li, Zuxing Gu, Min Zhou, Jiecheng Wu, Jiarui Zhang, Ming Gu. API Misuse Detection in C Programs: Practice on SSL APIs. IJSEKE 2019. [SCI收录,CCF C]

  7. Guang Chen, Yuexing Wang, Min Zhou, Jiaguang Sun. VFQL: Combinational Static Analysis as Query Language. In Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis(ISSTA), pp. 378-381. ACM, 2019. [EI收录,CCF A]

  8. Chi Li, Min Zhou, Zuxing Gu, Ming Gu. VBSAC: A Value-Based Static Analyzer for C. In Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis(ISSTA), pp. 382-385. ACM, 2019. [EI收录,CCF A]

  9. Zuxing Gu, Jiecheng Wu, Chi Li, Min Zhou, Ming Gu. SSLDoc: Automatically Diagnosing Incorrect SSL API Usages in C Programs. In Proceedings of 31st International Conference on Software Engineering & Knowledge Engineering (SEKE 2019). [EI收录,CCF C]

  10. Zuxing Gu, Jiecheng Wu, Jiaxiang Liu, Min Zhou, Ming Gu. An Empirical Study on API-Misuse Bugs in Open-Source C Programs. In Proceedings of 43rd IEEE Annual Computer Software and Application Conference (COMPSAC 2019). [EI收录,CCF C]

  11. Zuxing Gu, Min Zhou, Jiecheng Wu, Yu Jiang, Jiaxiang Liu, Ming Gu. IMSpec: An Extensible Approach to Exploring the Incorrect Usage of APIs. In Proceedings of 13th International Symposium on Theoretical Aspects of Software Engineering (TASE 2019). [EI收录,CCF C]

  12. Zuxing Gu, Jiecheng Wu, Li Chi, Min Zhou, Yu Jiang, Ming Gu, Jiaguang Sun. Vetting API Usages in C Programs with IMChecker. In Proceedings of the 41st International Conference on Software Engineering: Companion Proceedings(ICSE), pp. 91-94. IEEE Press, 2019. [EI收录,CCF A]

  13. Han Wang, Min Zhou, Xi Cheng, Guang Chen, and Ming Gu. Which Defect Should Be Fixed First? Semantic Prioritization of Static Analysis Report. In International Conference on Software Analysis, Testing, and Evolution, pp. 3-19. Springer, Cham, 2018. [EI收录]

  14. Guang Chen, Min Zhou, Jiaguang Sun and Xiaoyu Song. Scalable and Extensible Static Memory Safety Analysis with Summary Over Access Path. In 2018 25th Asia-Pacific Software Engineering Conference (APSEC), pp. 298-304. IEEE, 2018. [EI收录,CCF C]

  15. Xi Cheng, Min Zhou, Xiaoyu Song, Ming Gu, Jiaguang Sun. Tolerating C Integer Error via Precision Elevation. IEEE Transactions on Computers 68, no. 2 (2018): 270-286. [SCI收录,CCF A]

  16. Zuxing Gu, Yu Jiang, Min Zhou, Ming Gu, Xiaoyu Song, Lui Sha. A Cyber-Physical System Framework for Early Detection of Paroxysmal Diseases. IEEE Access, vol. 6, pp. 34834-34845. IEEE, 2018. [SCI收录]

  17. Xi Cheng, Min Zhou, Xioayu Song, Ming Gu, Jiaguang Sun. Parallelizing SMT Solving: Lazy decomposition and conciliation. Artificial Intelligence 257 (2018): 127-157. [SCI收录,CCF A]

  18. Yuexing Wang, Min Zhou, Xiaoyu Song, Ming Gu, Jiaguang Sun. Constructing Cost-Aware Functional Test-Suites Using Nested Differential Evolution Algorithm. IEEE Transactions on Evolutionary Computation. 22(3):334-346, 2018. [SCI收录,CCF B]

  19. Min Zhou, William N.N. Hung, Xiaoyu Song, Ming Gu and Jiaguang Sun. Temporal Coverage Analysis for Dynamic Verification. IEEE Transactions on Circuits and Systems II: Express Briefs. 2017 Aug 30. [SCI收录]

  20. Yuexing Wang, Min Zhou, Yu Jiang, Xiaoyu Song, Ming Gu, Jiaguang Sun. A Static Analysis Tool with Optimizations for Reachability Determination. Preceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering, Urbana-Champaign, IL, USA, 2017. IEEE Press, Piscataway, NJ, USA, 925-930. [EI收录, CCF A]

  21. Xi Cheng, Min Zhou, Xiaoyu Song, Ming Gu, Jiaguang Sun. IntPTI: Automatic Integer Error Repair with Proper-Type Inference. Preceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering, Urbana-Champaign, IL, USA, 2017. IEEE Press, Piscataway, NJ, USA, 996-1001. [EI收录,CCF A]

  22. Zhenpeng Fang, Xibin Zhao, Min Zhou. Infer Precise Program Invariant Using Abstract Interpretation with Recurrence Solving. Proceedings of the 41st IEEE Computer Software and Applications Conference, vol. 1, pp. 196-201. IEEE, 2017. [EI收录,CCF C]

  23. Yuexing Wang, Zuxing Gu, Xi Cheng, Min Zhou, Xiaoyu Song, Ming Gu and Jiaguang Sun. A Constraint-Pattern Based Method for Reachability Determination. Proceedings of the 41st IEEE Computer Software and Applications Conference, vol. 1, pp. 85-90. IEEE, 2017. [EI收录,CCF C,EI检索号20174304306998]

  24. Jiaxiang Liu, Min Zhou, Xiaoyu Song, Ming Gu and Jiaguang Sun. Formal Modeling and Verification of a Rate-Monotonic Scheduling Implementation with Real-Time Maude. IEEE Transactions on Industrial Electronics. 2017 Apr; 64(4): 3239-3249. [SCI收录,WOS检索号WOS:000397770200071,EI检索号20171****64091]

  25. Min Zhou, Xi Cheng, Xinrui Guo, Ming Gu, Hongyu Zhang, Xiaoyu Song. Improving Failure Detection by Automatically Generating Test Cases Near the Boundaries. Proceedings of the IEEE 40rd Computer Software and Applications Conference, Atlanta, Georgia USA, 2016. [EI收录]

  26. Xi Cheng, Min Zhou, Xiaoyu Song, Ming Gu, Jiaguang Sun. Automatic Fix for C Integer Errors by Precision Improvement. Proceedings of the IEEE 40rd Computer Software and Applications Conference, Atlanta, Georgia USA, 2016. [EI收录]

  27. Lifan Su, Min Zhou, Hai Wan, Ming Gu. Probabilistic Modeling and Optimization of Real-Time Protocol for Multifunction Vehicle Bus. Tsinghua Science and Technology. [SCI收录]

  28. Xinrui Guo, Min Zhou, Xiaoyu Song, Ming Gu, Jiaguang Sun. First, Debug the Test Oracle. IEEE Transaction on Software Engineering. 2015(99):1. [SCI收录, A类期刊]

  29. Rui Wang, Yong Guan, Min Zhou, Jie Zhang and Xiaoyu Song. A Component-based Modeling and Validation Method for PLC Systems. Journal of Applied Mathematics. 2014. [SCI收录]

  30. Min Zhou, Fei He, Xiaoyu Song, Shi He, Gangyi Chen, Ming Gu. Estimating the Volume of Solution Space for Satisfiability Modulo Linear Real Arithmetic. Theory of Computing Systems. 2014:1-25 [SCI收录] [online: 13 June 2014, published: February 2015, Volume 56, Issue 2, pp 347-371]

  31. Liangze Yin, Fei He, Min Zhou, and Ming Gu. Reusing search tree for incremental SAT solving of temporal induction. Proceedings of the 18th IEEE International Conference on Complex Computer Systems, Singapore, p4-13, 2013. [EI收录, 检索号13780287]

  32. Chen Su, Min Zhou, Liangze Yin, Hai Wan, Ming Gu. Modeling and verification of component-based systems with data passing using BIP. Proceedings of the 18th IEEE International Conference on Complex Computer Systems, Singapore, p4-13, 2013. [EI收录, 检索号13780308]

  33. Min Zhou, Hai Wan, Rui Wang, Xiaoyu Song, Chen Su, Ming Gu, Jiaguang Sun. Formal Component-based modeling and synthesis for PLC systems. Computers in Industry. 2013. [SCI源刊, 影响因子2.062, 检索号234WS]

  34. Min Zhou, Fei He, Bow-Yaw Wang, Ming Gu, Jiaguang Sun. Array theory of bounded elements and its application. Journal of Automated Reasoning. 2013(52):379-405. [SCI源刊, 影响因子0.567]

  35. Min Zhou, Fei He, Bow-Yaw Wang, Ming Gu, Jiaguang Sun. A unified framework for DPLL(T) + Certificates. Journal of Applied Mathematics. 2013. [影响引子0.837, 检索号158JL]

  36. Min Zhou, Hai Wan, Chen Su, Liangze Yin, Lianyi Zhang, Fei He, Ming Gu. Component-based modeling and code synthesis for cyclic programs. Proceedings of the IEEE 37rd Computer Software and Applications Conference, Kyoto, Japan, 2013. [EI收录, 检索号20133916789294, 会议最佳论文]

  37. Rui Wang, Min Zhou, Liangze Yin, Lianyi Zhang, Jiaguang Sun, Gu Ming, Marius Bozga. Modeling and validation of PLC-controlled systems: a case study. the 6th IEEE International Symposium on Theoretical Aspectes of Software Engineering, Beijing, China, p161-166, 2012. [EI收录, 检索号20124015533074]

  38. Min Zhou, Fei He, Ming Gu. An efficient resolution based algorithm for SAT. Proceedings of the 5th IEEE International Symposium on Theoretical Aspectes of Software Engineering, Xi’an, China, p66-67, 2011. [EI收录, 检索号20114414482156]

  39. Min Zhou, Fei He, Bow-Yaw Wang, Ming Gu. On array theory of bounded elements. Proceedings of Computer Aided Verification, Edinburgh, Scotland, p570-584, 2010. [EI收录, 检索号20103113108474, A类会议]

  40. Min Zhou, Fei He, Ming Gu, Xiaoyu Song. Translation-based model checking for PLC programs. Proceedings of the IEEE 33rd Computer Software and Applications Conference, Seattle, USA, p553-562, 2009. [EI收录, 检索号20094812499717]

参与的典型项目

国家科研项目
  1. 制造企业数据空间设计理论与方法,科技部重点研发项目(子课题负责人),2020-2023;

  2. 国产自主基础软件代码分析和漏洞挖掘系统研发,北京市科委项目(子课题负责人),2019-2020;

  3. 某项目,科技部重点研发项目(项目骨干),2017-2020;

  4. 嵌入式系统验证中的覆盖率分析方法研究,自然科学基金委青年科学基金(项目负责人),2015-2017

  5. 某某代码保证与演化,973项目(专题负责人),2015-2019;

企事业单位委托项目
  1. 恶意代码检测工具,中央国债登记结算有限公司,2021-2022;

  2. 源代码审计算法与工具研制,中央国债登记结算有限公司,2020-2021;

  3. 软件白盒自动化测试工具开发,中车青岛四方车辆研究所有限公司,2020-2020;

  4. 某算法测试评估平台方案设计与论证,中国人民解放军61646部队,2018-2018;

  5. XX15发控软件常见动态缺陷的形式化分析项目,中国航发控制系统研究所,2017-2018;

成果转化项目
  1. Tsmart代码静态分析工具许可,2018-2020;

  2. 代码分析验证支撑软件许可,2016-2017;

  3. AlgEval算法测评软件许可,2020-2024;

  4. 代码漏洞静态检测系统,2020-2020;