欢迎对模型算法、机器和模型学习以及智能系统验证等方面感兴趣的同学报考本实验室！

部分科研项目简介

• 国家自然科学基金项目“多时钟时间自动机的学习”2025/1-2028/12，第一负责人

• 国家自然基金重点项目“人机物三元融合场景的泛在计算抽象和软件定义方法”2021-2025，子课题负责人

• 国家自然科学基金项目“时间系统的模型学习”2020/1-2023/12，第一负责人

• 国家自然科学基金项目“扩展的线性时段不变式的模型检验”2015/1-2018/12，第一负责人

• 国家自然科学基金项目“基于构件的异构嵌入式系统的模型驱动设计”2011/1-2013/12，第一负责人

• 国家自然科学基金项目“基于概率时间自动机的概率时段演算的模型检验及应用研究”2007/1-2009/12，第一负责人

• 教育部留学回国人员科研启动基金

部分论文

• Jin Xu, Miaomiao Zhang, Bowen Du. SART: Sign-Absolute Reformulation Theory for Binary Variable Reduction in Neural Network Verification. Accepted by OOPSLA 2026.

• Yinghao Wu, Miaomiao Zhang, Fu Song, John Baugh. SmartIFSyn: Automated Information Flow Security Policy Synthesis for Smart Contracts. Accepted by FSE 2026.

• Xiaochen Tang, Zhenya Zhang, Miaomiao Zhang, Jie An. Control Synthesis of Cyber-Physical Systems for Real-Time Specifications through Causation-Guided Reinforcement Learning. To appear in Proceedings of RTSS 2025

• Ziran Wang, Jie An, Naijun Zhan, Miaomiao Zhang, Zhenya Zhang. On Synthesis of Timed Regular Expressions. To appear in Proceedings of RTSS 2025

• Junjie Meng, Jie An, Yong Li, Andrea Turrini, Miaomiao Zhang. SAT-Based Synthesis of Minimal Deterministic Real-Time Automata via 3DRTA Representation. Accepted by VMCAI 2026

• Hanyue Chen, Miaomiao Zhang, Frits W. Vaandrager. Compositional Abstraction for Timed Systems with Broadcast Synchronization. CAV (1) 2025: 162-184

• Hanyue Chen, Yu Su, Miaomiao Zhang, Zhiming Liu, Junri Mi. Learning Assumptions for Compositional Verification of Timed Automata. CAV (1) 2023: 40-61

• Yu Teng, Hanyue Chen, Junri Mi, Miaomiao Zhang, Jie An, Naijun Zhan. Active Learning of Deterministic Timed Automata via Timed Classification Tree. Science China Information Science 2025, 68:222101

• Junjie Meng, Jie An, Yong Li, Andrea Turrini, Fanjiang Xu, Naijun Zhan, Miaomiao Zhang. Efficient Decomposition Identification of Deterministic Finite Automata from Examples. To appear in Proceedings of SETTA 2025

• Yu Teng, Miaomiao Zhang, Jie An. Learning Deterministic Multi-Clock Timed Automata. HSCC 2024: 6:1-6:11

• Shaojun Deng, Wanwei Liu, Miaomiao Zhang. Runtime Verification of Neural-Symbolic Systems. SETTA 2024: 293-309

• Xiaochen Tang, Miaomiao Zhang, Wanwei Liu, Bowen Du, Zhiming Liu. Towards a Model of Human-Cyber-Physical Automata and a Synthesis Framework for Control Policies. J. Syst. Archit. 144: 102989 (2023)

• Miaomiao Zhang, Yu Teng, Hui Kong, John W. Baugh Jr., Yu Su, Junri Mi, Bowen Du. Automatic Modelling and Verification of AUTOSAR Architectures. J. Syst. Softw. 201: 111675 (2023)

• Jie An, Lingtai Wang, Bohua Zhan, Naijun Zhan, Miaomiao Zhang. Learning Real-Time Automata. Sci. China Inf. Sci. 64(9) (2021)

• Xiangyu Jin, Jie An, Bohua Zhan, Naijun Zhan, Miaomiao Zhang. Inferring Switched Nonlinear Dynamical Systems. Formal Aspects Comput. 33(3): 385-406 (2021)

• Jie An, Bohua Zhan, Naijun Zhan, Miaomiao Zhang. Learning Nondeterministic Real-Time Automata. ACM Trans. Embed. Comput. Syst. 20(5s): 99:1-99:26 (2021)

• Jian Wang, Jie An, Mingshuai Chen, Naijun Zhan, Lulin Wang, Miaomiao Zhang, Ting Gan. From Model to Implementation: a Network Algorithm Programming Language. Sci. China Inf. Sci. 63(7) (2020)

• Bai Xue, Miaomiao Zhang, Arvind Easwaran, Qin Li. PAC Model Checking of Black-Box Continuous-Time Dynamical Systems. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 39(11): 3944-3955 (2020)

• Wei Shen, Jie An, Bohua Zhan, Miaomiao Zhang, Bai Xue, Naijun Zhan. PAC Learning of Deterministic One-Clock Timed Automata. ICFEM 2020: 129-146

• Jin Xu, Zishan Li, Bowen Du, Miaomiao Zhang, Jing Liu. Reluplex Made More Practical: Leaky ReLU. ISCC 2020: 1-7

• Jie An, Mingshuai Chen, Bohua Zhan, Naijun Zhan, Miaomiao Zhang. Learning One-Clock Timed Automata. TACAS (1) 2020: 444-462

• Jie An, Naijun Zhan, Xiaoshan Li, Miaomiao Zhang, Wang Yi. Model Checking Bounded Continuous-Time Extended Linear Duration Invariants. HSCC 2018: 81-90

• Quan Zu, Miaomiao Zhang, Jiaqi Zhu, Naijun Zhan. Bounded Model-Checking of Discrete Duration Calculus. HSCC 2013: 213-222

• Jasper Berendsen, Biniam Gebremichael, Frits W. Vaandrager, Miaomiao Zhang. Formal Specification and Analysis of Zeroconf using UPPAALs. ACM Trans. Embed. Comput. Syst. 10(3): 34:1-34:32 (2011)

• Miaomiao Zhang, Zhiming Liu, Naijun Zhan. Model Checking Linear Duration Invariants of Networks of Automata. FSEN 2009: 244-259

• Miaomiao Zhang, Zhiming Liu, Charles Morisset, Anders P. Ravn. Design and Verification of Fault-Tolerant Components. Methods, Models and Tools for Fault Tolerance 2009: 57-84

• Miaomiao Zhang, Dang Van Hung, Zhiming Liu. Verification of Linear Duration Invariants by Model Checking CTL Properties. ICTAC 2008: 395-409

• Dang Van Hung, Miaomiao Zhang. On Verification of Probabilistic Timed Automata against Probabilistic Duration Properties. RTCSA 2007: 165-172