Contact

Email: yuanruizhang@nuaa.edu.cn, zhangyrmath@126.com

Address

College of Computer Science and Technology/College of Software, Nanjing University of Aeronautics and Astronautics (NUAA), Jiangjun Road No. 29, Jiangning District, Nanjing, China. Postal Code: 210016

Welcome to my home page. Here is the space for all of our research work and all academic-related information about me. One can also visit my current official website , or its english version .

I received my PhD degree from East China Normal University in 2019, majored in software engineering. From 2013 - 2014 I visited Team AOSTE at INRIA, Sophia Antipolis, France, and later worked as a post-doc researcher at Southwest University from 2019. Currently I am a lecturer at College of Software, Nanjing University of Aeronautics and Astronautics (NUAA), mainly working on formal specification and verification of software engineering. Up to now, I have published about 20 papers on journals and conferences in this area, including: Formal Aspects of Computing, Journal of Logical and Algebraic Methods in Programming, Science of Computer Programming, Frontiers of Computer Science, TASE, FTSCS, etc. And I have hosted one project of National Nature Science Foundation of China (Youth Project) and one project of National Science Foundation of Chongqing.

Education

2014 - 2019:
PhD in Software Engineering
East China Normal University, Shanghai, China
Dissertation: "Research on the Clock-constraint-based Dynamic Logic System for Synchronous Systems"
Advisor: Prof. Yixiang Chen
2013 - 2014:
Master of Science/Academic Visiting
Université Nice-Sophia-Antipolis (now "Université Côte d'Azur"), Nice, France
Major: Software Engineering (Informatique Fondements et Ingénierie)
Advisor: Prof. Frédéric Mallet
2012 - 2013:
(Studying as a master student)
East China Normal University (ECNU), Shanghai, China
Major: Software Engineering
Advisor: Prof. Yixiang Chen
2008 - 2012:
Bachelor of Science
University of Science and Technology Beijing, Beijing, China
Major: Pure and Applied Mathematics

Work Experience

2023 - now:
Lecturer
College of Computer Science and Technology/College of Software, University of Aeronautics and Astronautics (NUAA), Nanjing, China
2019 - 2023:
Post-doc Researcher
School of Mathematics and Statistics/RISE Lab, Southwest University, Chongqing, China
Advisor: Prof. Zhiming Liu
2013 - 2014:
Research Internship
Inria Centre at Université Nice-Sophia-Antipolis (now "Inria Centre at Université Côte d'Azur")
Advisor: Prof. Frédéric Mallet

Academic Work

  • PC member: AILA 2024
  • Reviewer: AILA 2024
  • Sub-reviewer: ICFEM 2024, SEFM 2023, ICFEM 2022, FACS 2022, ICTAC 2022, FACS 2021, SETTA 2020, SEH 2020, ICFEM2019, FACS 2019

Academic Activities

  • November 1st, 2024. Inviting Prof. Frederic Mallet to give a talk, titled ``Real-time CCSL: Application to the Mechanical Lung Ventilator'', at NUAA, Nanjing, China.
  • August, 2024. Participating the conference of Theoretical Aspects of Software Engineering Conference (TASE 2024) at Guiyang, Guizhou, China.
  • July, 2024. Participating the LEDS conference at Hulunbeier, InnerMongonia, China.
  • August, 2019. Presenting at the LEDS conference at Yili, XinJiang, China.
  • July, 2019. Participating the conference of Theoretical Aspects of Software Engineering Conference (TASE 2019) at Guilin, China, and giving a presentation.
  • April, 2017. Participating SETSS 2017 the 3rd international school at Chongqing, China.
  • April, 2016. Participating SETSS 2016 the 2nd international school at Chongqing, China.
  • October, 2015. Presenting at the conference of Requirements Engineering in the Big Data Era - Second Asia Pacifc Symposium, APRES 2015, at Wuhan, China.
  • 2013. Participating the DAESD Spring School 2013 at East China Normal University, Shanghai, China.

My research interests, in large scale, focus on logics and their related theories in computer science, encompassing dynamic logics, relational calculi, temporal logics, process algebras, etc. Particularly, I am interested in their applications for system/program specifications and verifications.

Up to now, our research work mainly includes the following aspects: Dynamic logics and deduction-based verification , where we develop verification methods and techniques for synchronous models of reactive systems using dynamic logics; Formal specification languages for Real-time Embedded Systems, where we create high-level formal specification languages and associated verification techniques to handle logical time constraints and properties of real-time embedded systems and system models; Proof theories of regular expressions , where we investigate proof theories of regular expression equations with respect to bisimulation equivalences.

Recently, we are interested in working on developing sound and effective logic theories, calculi, and related verification methods to address critical verification challenges in cyber-physical systems and systems with AI components.

Generally speaking, my research goal is to enhance the reliability and robustness of these systems through rigorous, logic-based methods.

Students Recruitment

I was looking for master students who have good mathematical background and who are interested in my research field. Please contact me through my email and send me your CV.

Manuscripts/Publications

  1. 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)
  2. Yuanrui Zhang . Parameterized Dynamic Logic --- Towards A Cyclic Logical Framework for General Program Specification and Verification . arXiv:2404.18098v3, 2024.
  3. 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)
  4. Yuanrui Zhang , Xinxin Liu. Image Reflection on Process Graphs -- A Novel Approach for the Completeness of an Axiomatization of 1-Free Regular Expressions Modulo Bisimilarity . arXiv:2311.01222v2, 2023.
  5. 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)
  6. 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)
  7. 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)
  8. Yuanrui Zhang . A Dynamic Logic for Verification of Synchronous Models based on Theorem Proving . arxiv: 2104.03681, 2021.
  9. 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)
  10. Bo Liu, Yuanrui Zhang , Xuelian Cao, Yu Liu, Bin Gu, Tiexin Wang. A Survey of ModelDriven Techniques and Tools for Cyber-Physical Systems. Frontiers of Information Technology & Electronic Engineering . val. 21, no. 11, pp. 1567-1590, 2020. (CCF C)
  11. 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)
  12. 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.
  13. 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.
  14. Yuanrui Zhang , Yujing Ma, Yixiang Chen. A UTP Refinement Model of the STeC Language . In Proc.: QRS Companion 2016, pp. 236-243, 2016.
  15. Kangli He, Yixiang Chen, Min Zhang, Yuanrui Zhang . PSTeC: A Location-Time Driven Modelling Formalism for Probabilistic Real-Time Systems . In Proc.: MMB/DFT 2016, pp. 77-91, 2016.
  16. 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.
  17. Yuanrui Zhang , Yixiang Chen, Yujing Ma. A Framework for Data-Driven Automata Design . In Proc.: APRES 2015, pp. 33-47, 2015.
  18. Yixiang Chen, Yuanrui Zhang . A Hybrid Clock System Related to STeC Language . In Proc.: SERE (Companion) 2014, pp. 199-203, 2014.
  19. 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)

Projects

2021 - now:
Host Youth Project of National Nature Science Foundation of China (国家自然科学青年基金项目), No. 62102329
Title: "A Verification Method for Synchronous Models Based on Dynamic Logic" (基于动态逻辑的同步模型验证方法)
2021 - now:
Host Project of National Science Foundation of Chongqing (重庆市自然科学博士后基金项目), No. cstc2021jcyj-bshX0120
Title: "Research on the Verification Method for Synchronous Models Based on Dynamic Logic" (基于动态逻辑的同步模型验证方法研究)
2023 - now:
Participate Project of National Nature Science Foundation of China (国家自然科学基金面上项目), No. 62272397
Title: "强化学习安全性的形式化方法研究及其在智能控制中的应用"
2013 - 2017:
Participate Project of National Nature Science Foundation of China (国家自然科学基金面上项目), No. 61370100
Title: "具有时空一致性的软件形式化理论和方法研究"

Students

2024:
  • Xin Wen (文馨) . Undergraduate student. Status: graduated.
    Title of thesis: "Esterel 语言的可执行语义及其在 Maude 上的实现".