Publications

Papers

• Zhe Chen, Yunlong Zhu, Zhemin Wang. Design and implementation of an aspect-oriented C programming language. In Proceedings of the ACM SIGPLAN International Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA 2024), Pasadena, California, United States, October 20–25, 2024, Proceedings of the ACM on Programming Languages (PACMPL), 8(OOPSLA1):117:1--28, ACM, 2024. [Artifact and Reproduction Package]
• Zhe Chen, Rui Yan, Yingzi Ma, Yulei Sui, Jingling Xue. A smart status based monitoring algorithm for the dynamic analysis of memory safety. ACM Transactions on Software Engineering and Methodology, 33(4):89:1--47, ACM, 2024.
• Shuanglong Kan, Zhe Chen, David Sanan, and Yang Liu. Formally understanding Rust's ownership and borrowing system at the memory level. Formal Methods in System Design, 64(1):200--236, Springer, 2024.
• Zhe Chen, Qi Zhang, Jun Wu, Junqi Yan, and Jingling Xue. A source-level instrumentation framework for the dynamic analysis of memory safety. IEEE Transactions on Software Engineering, 49(4):2107--2127, IEEE, 2023.
• Yiyu Zhang, Tianyi Liu, Zewen Sun, Zhe Chen, Xuandong Li, Zhiqiang Zuo. Catamaran: Low-overhead memory safety enforcement via parallel acceleration. In Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2023), Seattle, Washington, United States, July 17–21, 2023, pp. 816--828, ACM, 2023.
• Zhe Chen, Jun Wu, Qi Zhang, Jingling Xue. A dynamic analysis tool for memory safety based on smart status and source-level instrumentation. In Proceedings of the 44th ACM/IEEE International Conference on Software Engineering (ICSE 2022), DEMO Track, Pittsburgh, USA, May 22-27, 2022, Companion Volume, pp. 6--10, ACM, 2022.
• Xiaohua Yin, Zhiqiu Huang, Shuanglong Kan, Guohua Shen, Zhe Chen, Yang Liu, Fei Wang. SafeOSL: Ensuring memory safety of C via ownership-based intermediate language. Software-Practice & Experience, 52(5):1114--1142, Wiley, 2022.
• 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. [Artifact and Reproduction Package]
• 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, 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.
• 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.
• Ping Yin, Jacques Liandrat, Wanqiang Shen, Zhe Chen. A multiresolution and smooth fictitious domain method for one-dimensional elliptical and Stefan problems. Mathematical and Computer Modelling, 58(11-12):1727--1737, Elsevier, 2013.

Chinese Papers

• 殷家乐, 陈哲. 结合动态分析的内存安全漏洞模糊测试方法. 计算机科学, 52(11): 382-389, 2024.
• 严瑞, 陈哲. 多线程C程序内存安全性动态分析方法. 计算机科学, 51(S1): 803-808, 2024.
• 李佳洁, 陈哲, 陈龙腾. 一种基于无锁队列的运行时多线程并行验证方法. 小型微型计算机系统, 45(5): 1249-1256, 2024.
• 马莺姿, 陈哲, 殷家乐, 毛瑞琪. 结合模糊测试和动态分析的内存安全漏洞检测. 计算机科学, 51(2): 352-358, 2024.
• 孙毅, 陈哲, 冉丹, 杨志斌. 一种SCADE同步语言程序安全属性自动验证工具. 小型微型计算机系统, 43(4): 858-864, 2022.
• 冉丹, 陈哲, 孙毅, 杨志斌. 基于程序转化的SCADE模型检测. 计算机科学, 48(12): 125-130, 2021.
• 孙小祥, 陈哲. 基于定理证明的内存安全性动态检测算法的正确性研究. 计算机科学, 48(1): 268-272, 2021.
• 陈云云, 陈哲. 线性时序逻辑公式的可监控性量化算法. 小型微型计算机系统, 41(11): 2413-2419, 2020.
• 陈哲, 王冲, 黄志球. 基于动态分析的程序设计课程教学系统. 计算机系统应用, 29(10): 114-119, 2020.
• 杨志斌, 袁胜浩, 谢健, 周勇, 陈哲等. 一种同步语言多线程代码自动生成工具. 软件学报, 30(7): 1980-2002, 2019.
• 卜磊, 陈立前, 陈哲, 陈振邦, 冯新宇等. 形式化方法的研究进展与趋势. CCF 2017-2018中国计算机科学技术发展报告, 1-68, 2018.
• 严俊琦, 陈哲, 黄志球. C程序内存安全的运行时检测方法研究和实现. 小型微型计算机系统, 38(10): 2358-2362, 2017.
• 黄吴丹, 陈哲. 边界网关协议安全性的模型检验方法研究. 小型微型计算机系统, 38(06): 1187-1191, 2017.
• 李昕, 陈哲, 王哲民, 黄志球. 嵌套模式模板在运行时验证中的应用. 小型微型计算机系统, 38(03): 489-493, 2017.
• 王哲民, 陈哲, 朱云龙, 黄志球. 参数化运行时验证研究和工具实现. 小型微型计算机系统, 37(12): 2667-2672, 2016.
• 朱云龙, 陈哲, 王哲民, 李绪蓉, 黄志球. 针对C语言的面向方面语言设计与实现. 小型微型计算机系统, 37(12): 2679-2684, 2016.
• 陈光颖, 黄志球, 陈哲, 阚双龙. 面向DO-333的襟缝翼控制单元安全性分析. 计算机科学, 2016(5): 150-156, 2016.
• 马银雪, 陈哲, 黄志球, 黄吴丹. 使用模型检验自动化验证路由协议. 小型微型计算机系统, 36(11): 2462-2466, 2015.
• 马银雪, 李文明, 陈哲. 基于对象的C程序边界安全检测改进技术. 计算机与现代化, 2015(10): 25-30, 2015.
• 魏欧, 石玉峰, 徐丙凤, 黄志球, 陈哲. 软件模型检测中的抽象模型研究综述. 计算机研究与发展, 52(7): 1580-1603, 2015.
• 李文明, 陈哲, 李绪蓉, 黄志球. C程序数组越界的运行时验证技术研究与实现. 计算机工程与应用, 51(11): 190-195, 2015.
• 阚双龙, 黄志球, 陈哲, 徐丙凤. 使用事件自动机规约的C语言有界模型检测. 软件学报, 25(11): 2452-2472, 2014.
• 汪旺, 夏凤, 陈哲, 黄志球. 面向服务器集群的自动化测试监控平台的研究和实现. 计算机与现代化, 2014(9): 137-142, 2014.
• 李文明, 陈哲, 李绪蓉. 缓存区溢出研究与发展. 计算机应用研究, 31(9): 2561-2566, 2014.
• 王进, 黄志球, 唐佳俊, 陈哲, 肖芳雄. BPEL谓词约束建模及可行路径分析. 计算机研究与发展, 51(4): 838-847, 2014.
• 黄志球, 徐丙凤, 阚双龙, 胡军, 陈哲. 嵌入式机载软件安全性分析标准、方法及工具研究综述. 软件学报, 25(2): 200-218, 2014.
• 范大娟, 黄志球, 李清, 陈哲, 柯昌博. 支持语义、接口和协议的服务相容性分析. 解放军理工大学学报（自然科学版）, 14(2): 182-189. 2013.
• 马琳, 黄志球, 徐丙凤, 陈哲. 支持模型检测的故障树生成方法研究. 计算机与数字工程, 41(2): 257-260, 2013.
• 陈娟娟, 魏欧, 黄志球, 陈哲. 基于双格的多值模型的精化关系与对称化简. 计算机工程与应用, 49(22): 40-45, 2013.
• 吕威, 黄志球, 陈哲, 阚双龙, 魏欧. ESpin：基于SPIN的Eclipse模型检测环境. 计算机工程与应用, 49(7): 45-51, 2013.
• 肖芳雄, 李燕, 黄志球, 曹子宁, 陈哲, 范大娟. 基于时间概率代价进程代数的Web服务组合建模和分析. 计算机学报, 35(5): 918-936, 2012.

Patents

• 陈哲, 王安祺. 基于线程执行序列反馈的模糊测试方法. 专利号：202511886662.8. 专利申请日：2025.12.15
• 陈哲, 毛瑞琪. 结合静态指针分析的内存安全运行时检测加速方法及介质. 专利号：202411910962.0. 专利申请日：2024.12.24, 授权公告日：2025.11.25, 授权公告号：CN119903505B
• 陈哲, 殷家乐. 一种结合动态分析的内存安全漏洞模糊测试方法. 专利号：202411372498.4. 专利申请日：2024.09.29, 授权公告日：2025.11.28, 授权公告号：CN119473869B
• 陈哲, 严瑞. 多线程程序内存安全性动态分析方法. 专利号：202310934654.0. 专利申请日：2023.07.27
• 陈哲, 刘一辰. 面向内存错误检测的源代码语句插桩方法. 专利号：202310915701.7. 专利申请日：2023.07.25
• 陈哲, 马莺姿. 对包含特定语句的程序进行内存安全性动态分析的方法. 专利号：202310017945.3. 专利申请日：2023.01.07
• 陈哲, 李佳洁. 基于无锁队列和信号量机制的并行运行时验证方法. 专利号：202211676578.X. 专利申请日：2022.12.27
• 陈哲, 方雨瑶. 一种同步语言程序多属性增量模型检测方法. 专利号：202211523760.1. 专利申请日：2022.11.30
• 陈哲，冉丹，孙毅. 一种复杂同步语言程序的化简转化和自动验证方法. 专利号：ZL202011117839.5. 专利申请日：2020.10.19, 授权公告日：2022.04.08, 授权公告号：CN112306470B
• 陈哲，孙毅，冉丹. 一种基于可满足性求解的同步语言程序自动验证方法. 专利号：ZL202011103235.5. 专利申请日：2020.10.15, 授权公告日：2022.04.26, 授权公告号：CN112269734B
• 陈哲，王冲，孙小祥. 一种面向动态分析的源代码插桩改进方法. 专利号：ZL202010539967.2. 专利申请日：2020.06.15, 授权公告日：2021.06.22, 授权公告号：CN111736846B
• 陈哲，孙小祥，王冲. 一种面向程序内存安全性验证工具的静态优化方法. 专利号：ZL202010160648.0. 专利申请日：2020.03.10, 授权公告日：2021.06.22, 授权公告号：CN111443916B
• 陈哲，陈云云，吴逸凡. 一种运行时验证中性质的可监控性概率的度量方法. 专利号：ZL202010157636.2. 专利申请日：2020.03.09, 授权公告日：2021.07.20, 授权公告号：CN111352848B
• 陈哲，严俊琦，杨志斌，黄志球. 源代码中内存错误的自动检测和定位方法. 专利号：ZL201710079948.4. 专利申请日：2017.02.15, 授权公告日：2020.08.14, 授权公告号：CN106940654B
• 陈哲，朱云龙，魏欧，黄志球. 一种源代码中值计算错误的自动检测和定位方法. 专利号：ZL201410499170.9. 专利申请日：2014.09.25, 授权公告日：2018.03.02
• 陈哲，朱云龙，黄志球，魏欧. 复杂约束条件下多组件软件部署的自动化与自适应方法及其部署管理系统. 专利号：ZL201410500293.X. 专利申请日：2014.09.25, 授权公告日：2017.10.31
• 陈哲，李文明，黄志球. 数组越界错误的自动检测和校正方法. 专利号：ZL201410022323.0. 专利申请日：2014.01.17, 授权公告日：2016.08.24

Books

• 贺伟，陈哲，龚涛，戴博. 《ASP.NET 2.0网络编程入门与实践》. 清华大学出版社, 2007.
• 陈哲，戴博，龚涛. 《Visual C# 2005程序设计》. 清华大学出版社, 2007.
• 陈哲，杨成立，龚涛. 《ASP.NET程序员成长攻略》. 中国水利水电出版社, 2007.