张元睿，硕士生导师，2019年毕业于华东师范大学软件工程专业，获得博士学位。2013-2014年赴法国INRIA国家信息自动化研究所访问1年，2019-2023年在西南大学从事博士后研究工作。目前，已在软件工程形式化方法领域的国内外期刊会议发表论文20余篇，包括：Science of Computer Programming、Formal Aspects of Computing、Journal of Logical and Algebraic Methods in Programming、Frontier of Computer Science、TASE、QRS等。主持国家自然科学青年基金、重庆市自然科学博士后基金等项目资助。

招收硕士研究生1~2名。对软件工程形式化方法，系统规约与验证，定理证明技术感兴趣的研究生，可以通过邮件与我联系，将个人简历发至邮箱。

部分代表论文：

[1] Yuanrui Zhang, Hengyang Wu, Yixiang Chen, Frédéric Mallet. A Clock-based Dynamic Logic for Modelling and Verification of CCSL Specifications in Synchronous Systems . Science of Computer Programming. vol. 203, pp. 102591, 2021. (CCF B)

[2] Yuanrui Zhang, Frédéric Mallet, Huibiao Zhu, Yixiang Chen, Bo Liu, Zhiming Liu. A Clock-based Dynamic Logic for Schedulability Analysis of CCSL Specifications . Science of Computer Programming. vol. 202, pp. 102546, 2021. (CCF B)

[3] Yuanrui Zhang, Frédéric Mallet, Zhiming Liu. A Dynamic Logic for Verification of Synchronous Models based on Theorem Proving . Frontiers of Computer Science, vol. 16, no. 4, pp. 164407, 2022. (CCF B, JCR Q2)

[4] Yuanrui Zhang, Zhiming Liu. A Dynamic Logic with Branching Modalities . Journal of Logical and Algebraic Methods in Programming. vol. 136, pp. 100921, 2024. (JCR Q2)

[5] Yuanrui Zhang, Frédéric Mallet, Min Zhang, Zhiming Liu. Specification and Verification of Multiclock Systems using a Temporal Logic with Clock Constraints . Formal Aspects of Computing. vol. 36, no. 2, 2024. (CCF B)

[6] Yuanrui Zhang, Frédéric Mallet, Yixiang Chen. A Verification Framework for Spatio-Temporal Consistency Language with CCSL as a Specification Language . Frontiers of Computer Science, vol. 14, no. 1, pp. 105-129, 2020. (CCF B, JCR Q2)

[7] Yuanrui Zhang, Frédéric Mallet, Huibiao Zhu, Yixiang Chen. A Logical Approach for the Schedulability Analysis of CCSL . In Proc.: TASE 2019, pp. 25-32, 2019. (CCF C)

[8] Yuanrui Zhang, Yixiang Chen, Hengyang Wu. A Process Algebra With Qualitative Calculus for Modeling Spatio-Temporal Behaviour . IEEE Access. vol. 7, pp. 57172-57187, 2019. （JCR Q2)

[9] Yuanrui Zhang, Hengyang Wu, Yixiang Chen, Frédéric Mallet. Embedding CCSL into Dynamic Logic: A Logical Approach for the Verification of CCSL Specifications . In Proc.: FTSCS 2018, pp. 101-118, 2018.

[10] Jinyang Li, Yuanrui Zhang , Yixiang Chen. A Self-Adaptive Traffic Light Control System Based on Speed of Vehicles . In Proc.: QRS Companion 2016, pp. 382-388, 2016.

[11] Yuanrui Zhang, Frédéric Mallet, Yixiang Chen. Timed Automata Semantics of Spatial-Temporal Consistency Language STeC . In Proc.: TASE 2014, pp. 201-208, 2014. (CCF C)

部分主持项目：

2021-2024，国家自然科学青年基金，基于动态逻辑的同步模型验证方法，No. 62102329，主持

2021-2024，重庆市自然科学博士后基金项目，基于动态逻辑的同步模型验证方法研究，No. cstc2021jcyj-bshX0120，主持

其他论文成果见https://yuanruizhang5a.github.io/

• 
  

2008.9 -- 2012.6
北京科技大学       数学与应用数学       学士毕业       学士学位

2012.9 -- 2013.6
华东师范大学       软件工程       硕士研究生在读

2013.9 -- 2014.6
法国尼斯大学       软件工程       硕士研究生毕业       硕士学位

2014.9 -- 2019.6
华东师范大学       软件工程       博士毕业       博士学位

2024.1 -- 至今

南京航空航天大学      计算机科学与技术学院/软件学院      讲师

2019.9 -- 2023.6

西南大学      数学与统计学院      博士后研究员

软件工程形式化方法/安全攸关系统的规约与验证方法