Designing, Modelling and Verifying a Container Terminal System Using UPPAAL. - Quan Zu; Miaomiao Zhang 003; Jing Liu 012; Qingfeng Du (HASE, 2008)

Verification of Linear Duration Invariants by Model Checking CTL Properties. - Miaomiao Zhang 003; Dang Van Hung; Zhiming Liu 001 (ICTAC, 2008)

BAS: A Case Study for Modeling and Verification in Trustable Model Driven Development. - Dehui Du; Jing Liu 012; Honghua Cao; Miaomiao Zhang 003 (TTSS, 2008)

Formal Analysis of Services Compatibility. - Xueqiang Gong; Jing Liu 012; Miaomiao Zhang 003; Jueliang Hu (COMPSAC (2), 2009)

Model Checking Linear Duration Invariants of Networks of Automata. - Miaomiao Zhang 003; Zhiming Liu 001; Naijun Zhan (FSEN, 2009)

Design and Verification of Fault-Tolerant Components. - Miaomiao Zhang 003; Zhiming Liu 001; Charles Morisset; Anders P. Ravn (Methods, Models and Tools for Fault Tolerance, 2009)

Modeling and Verification of an Automatic Train Protection System. - Xijiao Xiong; Jing Liu 012; Miaomiao Zhang 003; Zuohua Ding (COMPSAC Workshops, 2010)

Formal Specification of Hybrid MARTE Statecharts. - Ziwei Liu; Jing Liu 012; Jifeng He 001; Frédéric Mallet; Miaomiao Zhang 003 (TASE, 2012)

Bounded model-checking of discrete duration calculus. - Quan Zu; Miaomiao Zhang 003; Jiaqi Zhu 001; Naijun Zhan (HSCC, 2013)

Dynamic Matchings in Left Weighted Convex Bipartite Graphs. - Quan Zu; Miaomiao Zhang 003; Bin Yu (FAW, 2014)

Fast Dynamic Weight Matchings in Convex Bipartite Graphs. - Quan Zu; Miaomiao Zhang 003; Bin Yu (MFCS (2), 2015)

Dynamic matchings in left vertex weighted convex bipartite graphs. - Quan Zu; Miaomiao Zhang 003; Bin Yu (J. Comb. Optim., 2016)

An Approach to Proving Proof Obligation of Hybrid Event B Based on Differential Invariants. - Jie Liu 013; Jing Liu 012; Miaomiao Zhang 003; Haiying Sun; Xiaohong Chen 007; Dehui Du; Mingsong Chen 001 (COMPSAC (1), 2017)

Model Checking Bounded Continuous-time Extended Linear Duration Invariants. - Jie An 001; Naijun Zhan; Xiaoshan Li; Miaomiao Zhang 003; Wang Yi 001 (HSCC, 2018)

A proof-based method of hybrid systems development using differential invariants. - Jie Liu 013; Jing Liu 012; Miaomiao Zhang 003; Haiying Sun; Xiaohong Chen 007; Dehui Du; Mingsong Chen 001 (Frontiers Comput. Sci., 2018)

RBML: A Refined Behavior Modeling Language for Safety-Critical Hybrid Systems. - Zhangtao Chen; Jing Liu 012; Xi Ding; Miaomiao Zhang 003 (APSEC, 2019)

High-Speed Rail Operating Environment Recognition Based on Neural Network and Adversarial Training. - Xiaoxue Hou; Jie An 001; Miaomiao Zhang 003; Bowen Du 002; Jing Liu 012 (ICTAI, 2019)

Real-Time System Modeling and Verification Through Labeled Transition System Analyzer. - Yilong Yang 001; Quan Zu; Wei Ke 001; Miaomiao Zhang 003; Xiaoshan Li (IEEE Access, 2019)

PAC Learning of Deterministic One-Clock Timed Automata. - Wei Shen; Jie An 001; Bohua Zhan; Miaomiao Zhang 003; Bai Xue 001; Naijun Zhan (ICFEM, 2020)

Reluplex made more practical: Leaky ReLU. - Jin Xu 002; Zishan Li; Bowen Du 002; Miaomiao Zhang 003; Jing Liu 012 (ISCC, 2020)

Learning One-Clock Timed Automata. - Jie An 001; Mingshuai Chen; Bohua Zhan; Naijun Zhan; Miaomiao Zhang 003 (TACAS (1), 2020)

From model to implementation: a network algorithm programming language. - Jian Wang 042; Jie An 001; Mingshuai Chen; Naijun Zhan; Lulin Wang; Miaomiao Zhang 003; Ting Gan (Sci. China Inf. Sci., 2020)

PAC Model Checking of Black-Box Continuous-Time Dynamical Systems. - Bai Xue 001; Miaomiao Zhang 003; Arvind Easwaran; Qin Li 002 (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2020)

Learning real-time automata. - Jie An 001; Lingtai Wang; Bohua Zhan; Naijun Zhan; Miaomiao Zhang 003 (Sci. China Inf. Sci., 2021)

Inferring Switched Nonlinear Dynamical Systems. - Xiangyu Jin; Jie An 001; Bohua Zhan; Naijun Zhan; Miaomiao Zhang 003 (Formal Aspects Comput., 2021)

Learning Nondeterministic Real-Time Automata. - Jie An 001; Bohua Zhan; Naijun Zhan; Miaomiao Zhang 003 (ACM Trans. Embed. Comput. Syst., 2021)

Learning Deterministic One-Clock Timed Automata via Mutation Testing. - Xiaochen Tang; Wei Shen; Miaomiao Zhang 003; Jie An 001; Bohua Zhan; Naijun Zhan (ATVA, 2022)

Human-Cyber-Physical Automata and Their Synthesis. - Miaomiao Zhang 003; Wanwei Liu; Xiaochen Tang; Bowen Du 002; Zhiming Liu 001 (ICTAC, 2022)

Learning Assumptions for Compositional Verification of Timed Automata. - Hanyue Chen; Yu Su; Miaomiao Zhang 003; Zhiming Liu 001; Junri Mi (CAV (1), 2023)

Automatic modelling and verification of Autosar architectures. - Miaomiao Zhang 003; Yu Teng; Hui Kong 007; John W. Baugh Jr.; Yu Su; Junri Mi; Bowen Du 002 (J. Syst. Softw., 2023)

Towards a model of human-cyber-physical automata and a synthesis framework for control policies. - Xiaochen Tang; Miaomiao Zhang 003; Wanwei Liu; Bowen Du 002; Zhiming Liu 001 (J. Syst. Archit., 2023)

Learning Deterministic Multi-Clock Timed Automata. - Yu Teng; Miaomiao Zhang 003; Jie An 001 (HSCC, 2024)

Runtime Verification of Neural-Symbolic Systems. - Shaojun Deng; Wanwei Liu; Miaomiao Zhang 003 (SETTA, 2024)