(Un)decidable Problems about Reachability of Quantum Systems. - Yangjia Li; Mingsheng Ying (CONCUR, 2014)

Termination of nondeterministic quantum programs. - Yangjia Li; Nengkun Yu; Mingsheng Ying (Acta Informatica, 2014)

Debugging Quantum Processes Using Monitoring Measurements. - Yangjia Li; Mingsheng Ying (CoRR, 2014)

Model-Checking Linear-Time Properties of Quantum Systems. - Mingsheng Ying; Yangjia Li; Nengkun Yu; Yuan Feng 001 (ACM Trans. Comput. Log., 2014)

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

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)

Approximate Bisimulation and Discretization of Hybrid CSP. - Gaogao Yan; Li Jiao; Yangjia Li; Shuling Wang 003; Naijun Zhan (FM, 2016)

A Theorem Prover for Quantum Hoare Logic and Its Applications. - Tao Liu; Yangjia Li; Shuling Wang 003; Mingsheng Ying; Naijun Zhan (CoRR, 2016)

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)

Generating semi-algebraic invariants for non-autonomous polynomial hybrid systems. - Qiuye Wang; Yangjia Li; Bican Xia; Naijun Zhan (J. Syst. Sci. Complex., 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)

Robust Non-termination Analysis of Numerical Software. - Bai Xue 001; Naijun Zhan; Yangjia Li; Qiuye Wang (SETTA, 2018)

Reasoning about Parallel Quantum Programs. - Mingsheng Ying; Yangjia Li (CoRR, 2018)

Algorithmic analysis of termination problems for quantum programs. - Yangjia Li; Mingsheng Ying (Proc. ACM Program. Lang., 2018)

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

Formal Verification of Quantum Algorithms Using Quantum Hoare Logic. - Junyi Liu 002; Bohua Zhan; Shuling Wang 003; Shenggang Ying; Tao Liu; Yangjia Li; Mingsheng Ying; Naijun Zhan (CAV (2), 2019)

Quantum Hoare Logic. - Junyi Liu 002; Bohua Zhan; Shuling Wang 003; Shenggang Ying; Tao Liu; Yangjia Li; Mingsheng Ying; Naijun Zhan (Arch. Formal Proofs, 2019)

Quantum Relational Hoare Logic with Expectations. - Yangjia Li; Dominique Unruh (ICALP, 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)

Exploiting Quantum Assertions for Error Mitigation and Quantum Program Debugging. - Peiyi Li 002; Ji Liu 007; Yangjia Li; Huiyang Zhou (ICCD, 2022)

A proof system for disjoint parallel quantum programs. - Mingsheng Ying; Li Zhou 013; Yangjia Li; Yuan Feng 001 (Theor. Comput. Sci., 2022)