Education
2007.7-2014.1 PhD in Computer Science, Department of Computer Science and Technology, Tsinghua University
2003.8-2007.7 Bachelor in Mathematics, Department of Mathematics, Tsinghua University
Professional Experience
2019.11-Present Research Associate Professor, School of Software, Tsinghua University
2016.1-2019.11 Research Assistant Professor, School of Software, Tsinghua University
2014.1-2016.1 Postdoc, School of Software, Tsinghua University
2011.6-2011.8 Research Intern, Verimage Lab in France
Research Intersets
Software static analysis, software engineering, formal method, software test
Personal Description
Dr. Min Zhou graduated from Tsinghua University with a bachelor degree in mathematics, and focused on software theory and formal techniques in his PhD career. He has published over 40 papers in top-tier international journals and conferences, including 23 papers in the past 5 years (8 in SCI journals and 15 in EI conferences; 10 in CCF A, 1 in CCF B and 8 in CCF C). According to the directory of recommended international academic conferences and journals issued by CCF, he has published papers including 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) and other top journals in software engineering, artificial intelligence, and computer theory, as well as top conferences in formal methods and software engineering such as CAV, ASE, ICSE, and ISSTA. His publications include many high impact factor papers, such as IEEE Transactions on Industrial Electronics (IF>8.2), IEEE Transactions on Evolutionary Computation (IF>11.5), etc.
In 2010, he presented his paper "On Array Theory of Bounded Elements" at CAV, which is the first long paper published by scholars in China Mainland since the conference was held. CAV is the top conference in the field of formalism (CCF A) and is highly recognized by the industry. The paper "Component-based Modeling and Code Synthesis for Cyclic Programs The paper "Component-based Modeling and Code Synthesis for Cyclic Programs" was awarded the best paper in COMPSAC 2013, which proposed a model-driven development approach for cyclic programs and gave a technical solution for modeling, analysis, verification, and code generation in the whole life cycle. Besides, his another paper, "Automatic Fix for C The paper "Automatic Fix for C Integer Errors by Precision Improvement" published in 2016 proposed a precision improvement based automatic fix for program defects and won the best paper of COMPSAC 2016. In 2017, he proposed a verification method for monotonic rate scheduling programs and verified the code implementation of the monotonic rate scheduling algorithm at the code implementation level for the first time, and the related paper was published in TIE. For the core technology of automatic theorem proving, i.e., Satisfiability Mode Theory (SMT), he conducted an in-depth study of its parallelization solution problem and formed a prototype tool. In 2018, he published the paper "Parallelizing SMT solving: Lazy decomposition and conciliation" in Artificial Intelligence. Two research works on integer defect repair were published in Transactions on Computers and Transactions on Dependable and Secure Computing in 2018 and 2019 respectively, which are important research works in the field of early automatic defect repair.
As for the transformation of scientific research results, he presided over the development of Tsmart code static analysis tool based on theoretical research results with fully independent intellectual property rights, which has excellent functions and performance. The tool participated in the NASAC (2018) "Source Code Vulnerability Detection Prototype Tool" competition, and won the first prize. The tool was certified by CWE-Compatibility and has been applied in several important industries: (1) evaluation of domestic operating systems: 13 identified code defects were successfully detected and 6 kernel defect analysis reports were submitted, which accelerated the process of independent control of domestic operating systems; (2) analysis and verification of aero-engine control systems: it was deployed in the China Institute of Aero-engine Control Systems to detect engine control codes; (3) Rail transportation embedded system code analysis: more than 300 memory security and other issues were detected in the energy-saving autopilot project of China CNR; (4) satellite remote sensing algorithm evaluation: building a business algorithm analysis and evaluation platform and assisting in holding related competitions; (5) financial security field: realizing applications on 8 projects of Central Government Bond Registration and Settlement Co. (6) In addition, the tool has detected more than 70 code defects in more than ten important open source projects such as Linux and OpenSSL, and most of them have been officially confirmed and fixed. The tool has been well recognized by several industrial application.
Selected Publications
Chi Li, Min Zhou, Xinrong Han, Ming Gu. Sensing Error Handling Bugs in SSL Library Usages. TrustCom 2021. [EI，CCF C]
Chi Li, Yuexing Wang, Min Zhou, Ming Gu. Scalable Fault Detection Based on Precise Access Path. APSEC 2021. [EI，CCF C]
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]
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]
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]
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]
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]
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]
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]
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]
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]
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]
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]
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]
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]
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]
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]
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]
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]
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]
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]
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]
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 Index 20174304306998]
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 Index WOS:000397770200071，EI Index 20171203464091]
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]
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]
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]
Xinrui Guo, Min Zhou, Xiaoyu Song, Ming Gu, Jiaguang Sun. First, Debug the Test Oracle. IEEE Transaction on Software Engineering. 2015(99):1. [SCI, CCF A]
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]
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]
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, Index 13780287]
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, Index 13780308]
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, IF 2.062, Index 234WS]
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, IF 0.567]
Min Zhou, Fei He, Bow-Yaw Wang, Ming Gu, Jiaguang Sun. A unified framework for DPLL(T) + Certificates. Journal of Applied Mathematics. 2013. [IF 0.837, Index 158JL]
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, Index 20133916789294, Best Paper Award]
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, Index 20124015533074]
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, Index 20114414482156]
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, Index 20103113108474, CCF A]
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, Index 20094812499717]
Selected Fundings
National Research Projects
Theory and methods of data space design for manufacturing enterprises. Key R&D Project of Ministry of Science and Technology (sub-project leader). 2020-2023.
Domestic software code analysis and vulnerability mining system development. Project of Beijing Municipal Science and Technology Commision (sub-project leader). 2020-2023.
***. Key R&D Project of Ministry of Science and Technology (sub-project leader). 2017-2020.
Study of coverage analysis methods in embedded system verification. National Science Foudation of China (young track) (leader). 2015-2017.
***. 973 Project (sub-project leader). 2015-2019.
Projects entrusted by enterprises and institutions
Malicious code detection tool. China Central Treasury Bond Depository and Clearing Co. LTD. 2021-2022.
Source code auditing algorithm and its tool. China Central Treasury Bond Depository and Clearing Co. LTD. 2020-2021.
Software white-box automation test tool. CRRC Qingdao Sifang Vehicle Research Institute Co. LTD. 2020-2020.
*** algorithm evaluation platform. Unit 61646 of the PLA. 2018-2018.
Formal method for *** software's dynamic defects. Avic Control System Research Institute. 2017-2018.
Commercialization of scientific and technological achievements
Software static analysis tool Tsmart licensing. 2018-2020.
Code analysis and verification software licensing. 2016-2017.
AlgEval algorithm evaluation software licensing. 2020-2024.
Program bug static detection system. 2020-2020.
