个人简历

博士毕业于法国国立应用科学院，获计算机科学博士学位，出国前曾就读于中南大学、上海交通大学。曾任职于微软亚洲研究院，法国国家科学研究中心系统分析与架构实验室（LAAS-CNRS），从事研究开发工作。主要研究兴趣包括计算机科学、软件工程、网络空间安全、程序设计语言与建模语言，人工智能，智能软件分析和验证等，及其在航空航天、信息安全、物联网等领域的应用。主持国家自然科学基金3项、参与3项。作为第一作者在SPE、COMPJ、IPL、FUIN、TSMJ、SL等著名国际学术期刊和ICSE、ISSTA、TACAS、SPIN、COMPSAC、ICFEM、TASE等著名国际会议和国内核心期刊发表了40余篇研究论文，获得2019年ACM SIGSOFT Distinguished Paper Award。现任中国计算机学会形式化方法专委会委员，曾任中国计算机学会中国软件大会优秀青年学者论坛主席。
承担的科研项目情况（部分）：
主持多项科研项目：
1. 国家自然科学基金：内存安全性和形式化规约的运行时验证（62172217），2022/01/01-2025/12/31，主持
2. 国家自然科学基金：航电系统软件可靠性的形式化验证技术研究（U1533130），2016/01/01-2018/12/31，主持
3. 国家自然科学基金：基于控制机制的软件可靠性新技术及其理论研究（61100034），2012/01/01-2014/12/31主持
4. 中央高校基本科研业务费人工智能+专项
5. 教育部留学回国人员科研启动基金项目
6. 中国博士后科学基金特别资助项目
7. 中国博士后科学基金项目
参与多项科研项目：
1. 国家自然科学基金：基于抽象的软件符号模型检测研究（61170043），2012/01/01-2015/12/31
2. 国家自然科学基金：M-可解性、M-计算复杂性与计算机科学的模型理论（61033002），2011/01/01-2014/12/31
3. 国家自然科学基金：概率进程演算的测试语义（60703033），2008/01/01-2010/12/31
教育经历
2007.8 -- 2010.7法国国立应用科学学院 计算机系统 博士研究生 工学博士
2006.9 -- 2011.2上海交通大学 计算机软件与理论 博士研究生 工学博士
2003.9 -- 2006.4中南大学 模式识别与智能系统 硕士研究生 工学硕士
1999.9 -- 2003.6中南大学 计算机科学与技术 大学本科 工学学士
工作经历
2011.2 -- 至今南京航空航天大学 计算机科学与技术学院
2006.3 -- 2006.9微软亚洲研究院 自然语言计算组
科研项目
[1]校准装置
[2]软件参数化和变量化需求规约的关键验证技术研究
[3]航电系统软件可靠性的形式化验证技术研究
[4]软件运行时验技术研究
[5]基于控制机制的软件可靠性新技术及其理论研究
[6]软件监测和控制技术及其理论研究
[7]软件监测和控制技术及其理论研究

研究领域

学科研究方向一：计算机科学与技术
计算机科学与技术，程序设计语言，建模语言，人工智能，自动推理和求解技术。
学科研究方向二：软件工程
软件工程，智能软件分析和验证，及其在航空航天软件工程中的应用。
学科研究方向三：网络空间安全
网络空间安全，信息安全，物联网安全，网络协议验证。
学科研究方向四：电子信息
包括以上研究方向的内容。"计算机科学与技术，软件工程"

近期论文

Zhe Chen, Chong Wang, Junqi Yan, Yulei Sui, Jingling Xue.Runtime Detection of Memory Errors with Smart Status.In Proceedings of the 30th ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2021), Virtual, Denmark, July 11–17, 2021, pp. 296-308. ACM, 2021.
Zhe Chen, Yunyun Chen, Robert Hierons, Yifan Wu.Four-valued monitorability of omega-regular languages.In Proceedings of the 22nd International Conference on Formal Engineering Methods (ICFEM 2020), Singapore, March 1-3, 2021, Lecture Notes in Computer Science, vol. 12531, pp. 198-214. Springer, 2020.
Zhe Chen, Junqi Yan, Shuanglong Kan, Ju Qian, Jingling Xue.Detecting Memory Errors at Runtime with Source-Level Instrumentation.In Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2019), July 15-19, 2019, pp. 341-351. ACM, 2019. (ACM SIGSOFT Distinguished Paper Award)
Zhe Chen, Yifan Wu, Ou Wei, Bin Sheng.Deciding Weak Monitorability for Runtime Verification.In Proceedings of the ACM/IEEE 40th International Conference on Software Engineering (ICSE 2018), Gothenburg, Sweden, May 27-June 3, 2018, Companion Volume, pp. 163-164. ACM, 2018.
Zhe Chen, Chuanqi Tao, Zhiyi Zhang, Zhibin Yang.Beyond Spatial and Temporal Memory Safety.In Proceedings of the ACM/IEEE 40th International Conference on Software Engineering (ICSE 2018), Gothenburg, Sweden, May 27-June 3, 2018, Companion Volume, pp. 189-190. ACM, 2018.
Zhe Chen, Junqi Yan, Wenming Li, Ju Qian, Zhiqiu Huang.Runtime verification of memory safety via source transformation.In Proceedings of the ACM/IEEE 40th International Conference on Software Engineering (ICSE 2018), Gothenburg, Sweden, May 27-June 3, 2018, Companion Volume, pp.264-265. ACM, 2018.
Ju Qian, Fusheng Lin, Changjian Li, Zhiyi Zhang, Zhe Chen.Generating Realistic Logically Unreasonable Faulty Data for Fault Injection.In Proceedings of the IEEE 42nd Annual Computer Software and Applications Conference (COMPSAC 2018), Tokyo, Japan, 23-27 July 2018, Volume 2, pp. 436-441. IEEE, 2018.
Zhe Chen.Parametric Runtime Verification is NP-complete and coNP-complete.Information Processing Letters, 123:14-20, Elsevier, 2017.
Shuanglong Kan, Zhiqiu Huang, Zhe Chen, Weiwei Li, Yutao Huang.Partial order reduction for checking LTL formulae with the next-time operator.Journal of Logic and Computation, 27(4):1095-1131, Oxford University Press, 2017.
Zhe Chen, Zhemin Wang, Yunlong Zhu, Hongwei Xi, Zhibin Yang.Parametric Runtime Verification of C Programs.In Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2016), Eindhoven, The Netherlands, April 2-8, 2016, Lecture Notes in Computer Science, vol. 9636, pp. 299-315. Springer, 2016.
Shuanglong Kan, Zhiqiu Huang, Zhe Chen.Partial Order Reduction for State/Event Systems.In Proceedings of the 18th International Conference on Formal Engineering Methods (ICFEM 2016), Tokyo, Japan, November 14-18, 2016, Lecture Notes in Computer Science, vol. 10009, pp. 329-345. Springer, 2016.
Zhe Chen, Yi Gu, Zhiqiu Huang, Jun Zheng, Chang Liu, Ziyi Liu.Model Checking Aircraft Controller Software: A Case Study.Software-Practice & Experience, 45(7):989-1017, Wiley, 2015.
Zhe Chen.Control Systems on Automata and Grammars.The Computer Journal, 58(1):75-94, Oxford University Press, 2015.
Zhe Chen, Daqiang Zhang and Yinxue Ma.Modeling and Analyzing the Convergence Property of the BGP Routing Protocol in SPIN.Telecommunication Systems, 58(3):205-217, Springer, 2015.
Zhe Chen, Ou Wei, Zhiqiu Huang, Hongwei Xi.Formal Semantics of Runtime Monitoring, Verification, Enforcement and Control.In Proceedings of the 9th International Symposium on Theoretical Aspects of Software Engineering (TASE 2015), September 12-14, 2015, pp. 63-70. IEEE Computer Society, 2015.
Zhe Chen, Daqiang Zhang, Rongbo Zhu, Yinxue Ma, Ping Yin and Feng Xie.A Review of Automated Formal Verification of Ad Hoc Routing Protocols for Wireless Sensor Networks.Sensor Letters, 11(5):752-764, American Scientific Publishers, 2013.
Daqiang Zhang, Hongyu Huang, Jingyu Zhou, Feng Xia, Zhe Chen.Detecting Hot Road Mobility of Vehicular Ad Hoc Networks.Mobile Networks and Applications, 18(6):803-813, Springer, 2013.
Daqiang Zhang, Zhijun Yang, Vaskar Raychoudhury, Zhe Chen, Jaime Lloret.An Energy-Efficient Routing Protocol Using Movement Trends in Vehicular Ad hoc Networks.The Computer Journal, 56(8):938-946, Oxford University Press, 2013.
Zhe Chen.On the Generative Power of ω-Grammars and ω-Automata.Fundamenta Informaticae, 111(2):119-145, IOS Press, 2011.
Zhe Chen, Gilles Motet.Towards Better Support for the Evolution of Safety Requirements via the Model Monitoring Approach.In Proceedings of the ACM/IEEE 32nd International Conference on Software Engineering (ICSE 2010), Cape Town, South Africa, vol. 2, pp. 219-222. ACM, 2010.
Zhe Chen, Gilles Motet.Nevertrace Claims for Model Checking.In Proceedings of the 17th International SPIN Workshop on Model Checking of Software (SPIN 2010), Enschede, The Netherlands, Lecture Notes in Computer Science, vol. 6349, pp. 162-179. Springer, 2010.
Zhe Chen, Gilles Motet.System Safety Requirements as Control Structures.In Proceedings of the 33rd Annual IEEE International Computer Software and Applications Conference (COMPSAC 2009), Seattle, Washington, USA, pp. 324-331. IEEE Computer Society, 2009.
[1] 陈哲,,等.The research of finite element model updating method considering the uncertainty.Zhendong Gongcheng Xuebao,2017
[2] 陈哲,,等.Structural dynamic model updating based on augmented SVM.J Vib Shock,2017
[3] 陈哲,,等.Detecting memory errors at runtime with source-level instrumentation.ISSTA - Proc. ACM SIGSOFT Int. Symp. Softw. Test. Anal.,2019
[4] 陈哲,,等.路由协议的自动形式化验证方法研究.计算机技术与发展,2017
[5] 陈哲,,等.嵌套模式模板在运行时验证中的应用.小型微型计算机系统,2017
[6] 陈哲,,等.边界网关协议安全性的模型检验方法研究.小型微型计算机系统,2017
[7] 陈哲,,等.Parametric runtime verification is NP-complete and coNP-complete.INFORMATION PROCESSING LETTERS,2017
[8] 陈哲,,等.C程序内存安全的运行时检测方法研究和实现.小型微型计算机系统,2017
[9] 陈哲,陈哲,陈哲等.Runtime verification of memory safety via source transformation.Proc Int Conf Software Eng,2018
[10] 陈哲,陈哲,陈哲等.Beyond spatial and temporal memory safety.Proc Int Conf Software Eng,2018
[11] 陈哲,陈哲,陈哲等.Deciding weak monitorability for runtime verification.Proc Int Conf Software Eng,2018