Contact

Email: yuanruizhang@nuaa.edu.cn

Office Address

Room 126, College of Computer Science and Technology/College of Software, Nanjing University of Aeronautics and Astronautics, Jiangjun Road No. 29, Jiangning District, Nanjing, China

Here is where I put all of my research work and all academic-related information about me, just in case anyone would like to check.

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, ICFEM, 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. I was a PC member and a reviewer of conference AILA 2024, and was invited as the reviewers of the following conferences: ICFEM 2024, SEFM 2023, ICFEM 2022, FACS 2022, ICTAC 2022, FACS 2021, SETTA 2020, SEH 2020, ICFEM2019, FACS 2019.

News

  • 20240807: Posted another version (version 3) from the last one by fixing some minor errors and making some small modifications.
  • 20240708: Recently I submitted a new version of the manuscript about the parameterization of dynamic logics: version 2, please check here .
  • 20240622: Build this page.

My Favorite Quote

"You can't know everything, but you should convince yourself that you can know anything." --- John Carmack

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
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, 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 Activities

  • 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. Participating the LEDS conference at Yili, XinJiang, China, and giving a presentation.
  • 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. Participating the conference of Requirements Engineering in the Big Data Era - Second Asia Pacifc Symposium, APRES 2015, at Wuhan, China, and giving a presentation.
  • 2013. Participating the DAESD Spring School 2013 at East China Normal University, Shanghai, China.

Awards (During Student Time)

  • 2014 - 2016: Academic Scholarships of the East China Normal University (华东师范大学研究生学业奖学金) for 3 years, one first-class (一等奖) (in 2015) and two second-classes (二等奖).
  • 2016: Funding Support of the Excellent Doctorial Dissertations of the East China Normal University (华东师范大学优秀博士论文培育项目资助).
  • 2012: Outstanding Graduate of the University of Science & Technology Beijing (北京科技大学优秀毕业生).
  • 2008 - 2010: `Renmin' Scholarships of the University o Science & Technology Beijing (北京科技大学"人民"奖学金) for 3 years, one second-class (二等奖) (in 2009) and two third-classes (三等奖).
  • 2008: Tri-good Student of Haidian District of Beijing (北京市海淀区三好学生).

Skills

Programming Languages:
Familiar with Coq, Maude, UPPAAL; Familiar with C/C++, Java, Python.
Language Skills:
Able to communicate with English and Chinese. English Tests: CET 4 --- 564, CET 6 --- 477. ILETS --- 6.0.

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

Currently, my research work 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 , where we create high-level formal specification languages and associated verification techniques to handle logical time constraints and properties of systems and system models; Proof theories of regular expressions , where we investigate proof theories of regular expression equations with respect to bisimulation equivalences.

Additionally, I am working on developing sound and effective logic theories, calculi, and related verification methods to address critical verification challenges in probabilistic programs and AI systems.

My goal is to enhance the reliability and robustness of these systems through rigorous, logic-based deductive 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 上的实现".