从事软件工程形式化方法中，基于定理证明的系统规约验证方法的研究。具体地，旨在运用动态逻辑、Hoare逻辑、时态逻辑、Kleene代数等数学理论及由其衍生的技术手段，对各类软件系统、程序和模型进行系统行为描述、性质刻画、分析和验证。目前主要工作有：1. 动态逻辑和相关推理验证技术：我们发展了基于动态逻辑的同步系统规约与验证技术；2. 形式化规约语言：我们提出了一种高抽象层的形式化规约语言，用以对实时系统中的逻辑时钟约束及性质进行刻画，并发展相关验证技术；3. 正则表达式的等式证明理论：我们主要对正则表达式等式证明系统在互摸拟下的完备性进行了研究。

招收硕士研究生。欢迎有较好数学基础(离散数学、数理逻辑)，对软件工程形式化方法领域有一定了解，并对我的研究方向感兴趣的研究生加入。有意者可以通过邮件交流，并将个人简历发我。

代表性论文见"论文成果"页，主持项目见"科研项目"页。更详细的信息，见我的主页(保持及时更新)：https://yuanruizhang5a.github.io