Decidability of the Reachability for a Family of Linear Vector Fields. - Ting Gan; Mingshuai Chen; Liyun Dai; Bican Xia; Naijun Zhan (ATVA, 2015)

Termination Analysis of Polynomial Programs with Equality Conditions. - Yangjia Li; Hui Lu; Naijun Zhan; Mingshuai Chen; Guohua Wu (CoRR, 2015)

Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF. - Ting Gan; Liyun Dai; Bican Xia; Naijun Zhan; Deepak Kapur; Mingshuai Chen (IJCAR, 2016)

Computing reachable sets of linear vector fields revisited. - Ting Gan; Mingshuai Chen; Yangjia Li; Bican Xia; Naijun Zhan (ECC, 2016)

Validated Simulation-Based Verification of Delayed Differential Dynamics. - Mingshuai Chen; Martin Fränzle; Yangjia Li; Peter Nazier Mosaad; Naijun Zhan (FM, 2016)

A Two-Way Path Between Formal and Informal Design of Embedded Systems. - Mingshuai Chen; Anders P. Ravn; Shuling Wang 003; Mengfei Yang; Naijun Zhan (UTP, 2016)

Interpolation synthesis for quadratic polynomial inequalities and combination with textit{EUF}. - Ting Gan; Liyun Dai; Bican Xia; Naijun Zhan; Deepak Kapur; Mingshuai Chen (CoRR, 2016)

MARS: A Toolchain for Modelling, Analysis and Verification of Hybrid Systems. - Mingshuai Chen; Xiao Han 003; Tao Tang 004; Shuling Wang 003; Mengfei Yang; Naijun Zhan; Hengjun Zhao; Liang Zou (Provably Correct Systems, 2017)

Safe Over- and Under-Approximation of Reachable Sets for Delay Differential Equations. - Bai Xue 001; Peter Nazier Mosaad; Martin Fränzle; Mingshuai Chen; Yangjia Li; Naijun Zhan (FORMATS, 2017)

What's to Come is Still Unsure - Synthesizing Controllers Resilient to Delayed Interaction. - Mingshuai Chen; Martin Fränzle; Yangjia Li; Peter Nazier Mosaad; Naijun Zhan (ATVA, 2018)

Reachability Analysis for Solvable Dynamical Systems. - Ting Gan; Mingshuai Chen; Yangjia Li; Bican Xia; Naijun Zhan (IEEE Trans. Autom. Control., 2018)

NIL: Learning Nonlinear Interpolants. - Mingshuai Chen; Jian Wang 042; Jie An 001; Bohua Zhan; Deepak Kapur; Naijun Zhan (CADE, 2019)

Taming Delays in Dynamical Systems - Unbounded Verification of Delay Differential Equations. - Shenghua Feng; Mingshuai Chen; Naijun Zhan; Martin Fränzle; Bai Xue 001 (CAV (1), 2019)

In memory of Oded Maler: automatic reachability analysis of hybrid-state automata. - Martin Fränzle; Mingshuai Chen; Paul Kröger (ACM SIGLOG News, 2019)

Unbounded-Time Safety Verification of Stochastic Differential Dynamics. - Shenghua Feng; Mingshuai Chen; Bai Xue 001; Sriram Sankaranarayanan 001; Naijun Zhan (CAV (2), 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)

Latticed k-Induction with an Application to Probabilistic Programs. - Kevin Batz; Mingshuai Chen; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Christoph Matheja; Philipp Schröer (CAV (2), 2021)

Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming. - Qiuye Wang; Mingshuai Chen; Bai Xue 001; Naijun Zhan; Joost-Pieter Katoen (CAV (1), 2021)

Indecision and delays are the parents of failure - taming them algorithmically by synthesizing delay-resilient control. - Mingshuai Chen; Martin Fränzle; Yangjia Li; Peter Nazier Mosaad; Naijun Zhan (Acta Informatica, 2021)

Does a Program Yield the Right Distribution? - Verifying Probabilistic Programs via Generating Functions. - Mingshuai Chen; Joost-Pieter Katoen; Lutz Klinkenberg; Tobias Winkler 001 (CAV (1), 2022)

PA-Boot: A Formally Verified Authentication Protocol for Multiprocessor Secure Boot. - Zhuoruo Zhang; Chenyang Yu; He Huang; Rui Chang; Mingshuai Chen; Qinming Dai; Wenbo Shen; Yongwang Zhao; Kui Ren 001 (CoRR, 2022)

Encoding inductive invariants as barrier certificates: Synthesis via difference-of-convex programming. - Qiuye Wang; Mingshuai Chen; Bai Xue 001; Naijun Zhan; Joost-Pieter Katoen (Inf. Comput., 2022)

Prodigy - Artifact Evaluation at CAV 2022. - Mingshuai Chen; Joost-Pieter Katoen; Lutz Klinkenberg; Tobias Winkler 001 (Zenodo, 2022)

Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants. - Kevin Batz; Mingshuai Chen; Sebastian Junges; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Christoph Matheja (TACAS (2), 2023)

Exact Probabilistic Inference Using Generating Functions. - Lutz Klinkenberg; Tobias Winkler 001; Mingshuai Chen; Joost-Pieter Katoen (CoRR, 2023)

Exact Bayesian Inference for Loopy Probabilistic Programs. - Lutz Klinkenberg; Christian Blumenthal; Mingshuai Chen; Joost-Pieter Katoen (CoRR, 2023)

Lower Bounds for Possibly Divergent Probabilistic Programs. - Shenghua Feng; Mingshuai Chen; Han Su 003; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Naijun Zhan (Proc. ACM Program. Lang., 2023)

QuFEM: Fast and Accurate Quantum Readout Calibration Using the Finite Element Method. - Siwei Tan; Liqiang Lu; Hanyu Zhang; Jia Yu; Congliang Lang; Yongheng Shang; Xinkui Zhao; Mingshuai Chen; Yun Liang 001; Jianwei Yin (ASPLOS (2), 2024)

MorphQPV: Exploiting Isomorphism in Quantum Programs to Facilitate Confident Verification. - Siwei Tan; Debin Xiang; Liqiang Lu; Junlin Lu; Qiuping Jiang; Mingshuai Chen; Jianwei Yin (ASPLOS (3), 2024)

A Unified Framework for Quantitative Analysis of Probabilistic Programs. - Shenghua Feng; Tengshun Yang; Mingshuai Chen; Naijun Zhan (Principles of Verification (1), 2024)

Proving Functional Program Equivalence via Directed Lemma Synthesis. - Yican Sun; Ruyi Ji; Jian Fang; Xuanlin Jiang; Mingshuai Chen; Yingfei Xiong 001 (FM (1), 2024)

Horae: A Domain-Agnostic Modeling Language for Automating Multimodal Service Regulation⋆. - Yutao Sun; Mingshuai Chen; Kangjia Zhao; Jintao Chen (ICWS, 2024)

Parf: Adaptive Parameter Refining for Abstract Interpretation. - Zhongyi Wang 004; Linyu Yang; Mingshuai Chen; Yixuan Bu; Zhiyang Li; Qiuye Wang; Shengchao Qin; Xiao Yi; Jianwei Yin (ASE, 2024)

UniGM: Unifying Multiple Pre-trained Graph Models via Adaptive Knowledge Aggregation. - Jintao Chen; Fan Wang 020; Shengye Pang; Siwei Tan; Mingshuai Chen; Tiancheng Zhao; Meng Xi 002; Jianwei Yin (ACM Multimedia, 2024)

Fuzzy kernel evidence Random Forest for identifying pseudouridine sites. - Mingshuai Chen; Mingai Sun; Xi Su; Prayag Tiwari; Yijie Ding (Briefings Bioinform., 2024)

HORAE: A Domain-Agnostic Modeling Language for Automating Multimodal Service Regulation. - Yutao Sun; Mingshuai Chen; Kangjia Zhao; He Li; Jintao Chen; Linyu Yang; Zhongyi Wang 004; Tiancheng Zhao; Jianwei Yin (CoRR, 2024)

Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions. - Lutz Klinkenberg; Christian Blumenthal; Mingshuai Chen; Darion Haase; Joost-Pieter Katoen (Proc. ACM Program. Lang., 2024)

PseU-KeMRF: A Novel Method for Identifying RNA Pseudouridine Sites. - Mingshuai Chen; Quan Zou 001; Ren Qi; Yijie Ding (IEEE ACM Trans. Comput. Biol. Bioinform., 2024)

Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions Artifact. - Lutz Klinkenberg; Christian Blumenthal; Mingshuai Chen; Darion Haase; Joost-Pieter Katoen (Zenodo, 2024)

Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions Artifact. - Lutz Klinkenberg; Christian Blumenthal; Mingshuai Chen; Darion Haase; Joost-Pieter Katoen (Zenodo, 2024)

The Self-Improvement Paradox: Can Language Models Bootstrap Reasoning Capabilities without External Scaffolding? - Yutao Sun; Mingshuai Chen; Tiancheng Zhao; Ruochen Xu; Zilun Zhang; Jianwei Yin (ACL (Findings), 2025)

On the Almost-Sure Termination of Probabilistic Counter Programs. - Sergei Novozhilov; Mingqi Yang; Mingshuai Chen; Zhiyang Li; Jianwei Yin (CAV (2), 2025)

PARF: An Adaptive Abstraction-Strategy Tuner for Static Analysis. - Zhong-Yi Wang 004; Mingshuai Chen; Tengjie Lin; Linyu Yang; Junhao Zhuo; Qiuye Wang; Shengchao Qin; Xiao Yi; Jianwei Yin (CoRR, 2025)

Derivative-Agnostic Inference of Nonlinear Hybrid Systems. - Hengzhi Yu; Bohan Ma; Mingshuai Chen; Jie An 001; Bin Gu 006; Naijun Zhan; Jianwei Yin (CoRR, 2025)

Preguss: It Analyzes, It Specifies, It Verifies. - Zhongyi Wang 004; Tengjie Lin; Mingshuai Chen; Mingqi Yang; Haokun Li; Xiao Yi; Shengchao Qin; Jianwei Yin (CoRR, 2025)