Process Algebra Approach to Reasoning About Concurrent Actions. - Yuan Feng 001; Mingsheng Ying (J. Comput. Sci. Technol., 2004)

Proof rules for purely quantum programs - Yuan Feng 001; Runyao Duan; Zheng-Feng Ji; Mingsheng Ying (CoRR, 2005)

Catalyst-assisted probabilistic entanglement transformation. - Yuan Feng 001; Runyao Duan; Mingsheng Ying (IEEE Trans. Inf. Theory, 2005)

Probabilistic bisimilarities between quantum processes - Yuan Feng 001; Runyao Duan; Zheng-Feng Ji; Mingsheng Ying (CoRR, 2006)

Some Issues in Quantum Information Theory. - Runyao Duan; Zheng-Feng Ji; Yuan Feng 001; Mingsheng Ying (J. Comput. Sci. Technol., 2006)

Partial Recovery of Quantum Entanglement. - Runyao Duan; Yuan Feng 001; Mingsheng Ying (IEEE Trans. Inf. Theory, 2006)

Probabilistic bisimulations for quantum processes. - Yuan Feng 001; Runyao Duan; Zheng-Feng Ji; Mingsheng Ying (Inf. Comput., 2007)

Commutativity of quantum weakest preconditions. - Mingsheng Ying; Jianxin Chen; Yuan Feng 001; Runyao Duan (Inf. Process. Lett., 2007)

Proof rules for the correctness of quantum programs. - Yuan Feng 001; Runyao Duan; Zheng-Feng Ji; Mingsheng Ying (Theor. Comput. Sci., 2007)

Parameter Estimation of Quantum Channels. - Zheng-Feng Ji; Guoming Wang; Runyao Duan; Yuan Feng 001; Mingsheng Ying (IEEE Trans. Inf. Theory, 2008)

Locally undetermined states, generalized schmidt decomposition, and application in deistributed comuting. - Yuan Feng 001; Runyao Duan; Mingsheng Ying (Quantum Inf. Comput., 2009)

An Algebraic Language for Distributed Quantum Computing. - Mingsheng Ying; Yuan Feng 001 (IEEE Trans. Computers, 2009)

Distinguishability of Quantum States by Separable Operations. - Runyao Duan; Yuan Feng 001; Yu Xin; Mingsheng Ying (IEEE Trans. Inf. Theory, 2009)

Characterizing locally indistinguishable orthogonal product states. - Yuan Feng 001; Yaoyun Shi (IEEE Trans. Inf. Theory, 2009)

An algebra of quantum processes. - Mingsheng Ying; Yuan Feng 001; Runyao Duan; Zheng-Feng Ji (ACM Trans. Comput. Log., 2009)

Quantum loop programs. - Mingsheng Ying; Yuan Feng 001 (Acta Informatica, 2010)

A Flowchart Language for Quantum Programming. - Mingsheng Ying; Yuan Feng 001 (IEEE Trans. Software Eng., 2011)

Open Bisimulation for Quantum Processes. - Yuxin Deng; Yuan Feng 001 (IFIP TCS, 2012)

Defining Quantum Control Flow - Mingsheng Ying; Nengkun Yu; Yuan Feng 001 (CoRR, 2012)

Bisimulation for Quantum Processes. - Yuan Feng 001; Runyao Duan; Mingsheng Ying (ACM Trans. Program. Lang. Syst., 2012)

A Discrete Event Simulation Based Production Line Optimization through Markov Decision Process. - Yuan Feng 001; Wenhui Fan; Yuanhui Qin (AsiaSim, 2013)

Reachability Probabilities of Quantum Markov Chains. - Shenggang Ying; Yuan Feng 001; Nengkun Yu; Mingsheng Ying (CONCUR, 2013)

Quantum Information-Flow Security: Noninterference and Access Control. - Mingsheng Ying; Yuan Feng 001; Nengkun Yu (CSF, 2013)

Reachability Analysis of Recursive Quantum Markov Chains. - Yuan Feng 001; Nengkun Yu; Mingsheng Ying (MFCS, 2013)

A tighter bound for the self-stabilization time in Herman's algorithm. - Yuan Feng 001; Lijun Zhang 001 (Inf. Process. Lett., 2013)

Model checking quantum Markov chains. - Yuan Feng 001; Nengkun Yu; Mingsheng Ying (J. Comput. Syst. Sci., 2013)

Verification of quantum programs. - Mingsheng Ying; Nengkun Yu; Yuan Feng 001; Runyao Duan (Sci. Comput. Program., 2013)

Perturbation Analysis in Verification of Discrete-Time Markov Chains. - Taolue Chen 001; Yuan Feng 001; David S. Rosenblum; Guoxin Su (CONCUR, 2014)

When Equivalence and Bisimulation Join Forces in Probabilistic Automata. - Yuan Feng 001; Lijun Zhang 001 (FM, 2014)

Alternation in Quantum Programming: From Superposition of Data to Superposition of Programs. - Mingsheng Ying; Nengkun Yu; Yuan Feng 001 (CoRR, 2014)

Symbolic Bisimulation for Quantum Processes. - Yuan Feng 001; Yuxin Deng; Mingsheng Ying (ACM Trans. Comput. Log., 2014)

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

Decentralized Bisimulation for Multiagent Systems. - Lei Song 001; Yuan Feng 001; Lijun Zhang 001 (AAMAS, 2015)

On Coinduction and Quantum Lambda Calculi. - Yuxin Deng; Yuan Feng 001; Ugo Dal Lago (CONCUR, 2015)

Toward Automatic Verification of Quantum Cryptographic Protocols. - Yuan Feng 001; Mingsheng Ying (CONCUR, 2015)

QPMC: A Model Checker for Quantum Programs and Protocols. - Yuan Feng 001; Ernst Moritz Hahn; Andrea Turrini; Lijun Zhang 001 (FM, 2015)

Planning for Stochastic Games with Co-Safe Objectives. - Lei Song 001; Yuan Feng 001; Lijun Zhang 001 (IJCAI, 2015)

Extend Transferable Belief Models with Probabilistic Priors. - Chunlai Zhou; Yuan Feng 001 (UAI, 2015)

Distribution-based Bisimulation and Bisimulation Metric in Probabilistic Automata. - Yuan Feng 001; Lei Song 001; Lijun Zhang 001 (CoRR, 2015)

Quantum Privacy-Preserving Data Mining. - Shenggang Ying; Mingsheng Ying; Yuan Feng 001 (CoRR, 2015)

A nearly optimal upper bound for the self-stabilization time in Herman's algorithm. - Yuan Feng 001; Lijun Zhang 001 (Distributed Comput., 2015)

Quantum Markov chains: Description of hybrid systems, decidability of equivalence, and model checking linear-time properties. - Lvzhou Li; Yuan Feng 001 (Inf. Comput., 2015)

On hybrid models of quantum finite automata. - Lvzhou Li; Yuan Feng 001 (J. Comput. Syst. Sci., 2015)

An Iterative Decision-Making Scheme for Markov Decision Processes and Its Application to Self-adaptive Systems. - Guoxin Su; Taolue Chen 001; Yuan Feng 001; David S. Rosenblum; P. S. Thiagarajan (FASE, 2016)

Verify LTL with Fairness Assumptions Efficiently. - Yong Li 031; Lei Song 001; Yuan Feng 001; Lijun Zhang 001 (TIME, 2016)

Asymptotic Perturbation Bounds for Probabilistic Model Checking with Empirically Determined Probability Parameters. - Guoxin Su; Yuan Feng 001; Taolue Chen 001; David S. Rosenblum (IEEE Trans. Software Eng., 2016)

Model Checking Omega-regular Properties for Quantum Markov Chains . - Yuan Feng 001; Ernst Moritz Hahn; Andrea Turrini; Shenggang Ying (CONCUR, 2017)

ProEva: runtime proactive performance evaluation based on continuous-time markov chains. - Guoxin Su; Taolue Chen 001; Yuan Feng 001; David S. Rosenblum (ICSE, 2017)

Bisimulations for probabilistic linear lambda calculi. - Yuxin Deng; Yuan Feng 001 (TASE, 2017)

Quantum Privacy-Preserving Data Analytics. - Shenggang Ying; Mingsheng Ying; Yuan Feng 001 (CoRR, 2017)

Quantum Privacy-Preserving Perceptron. - Shenggang Ying; Mingsheng Ying; Yuan Feng 001 (CoRR, 2017)

Probabilistic bisimilarity as testing equivalence. - Yuxin Deng; Yuan Feng 001 (Inf. Comput., 2017)

Precisely deciding CSL formulas through approximate model checking for CTMCs. - Yuan Feng 001; Lijun Zhang 001 (J. Comput. Syst. Sci., 2017)

Model Checking Probabilistic Epistemic Logic for Probabilistic Multiagent Systems. - Chen Fu; Andrea Turrini; Xiaowei Huang 001; Lei Song 001; Yuan Feng 001; Lijun Zhang 001 (IJCAI, 2018)

Model Checking Quantum Systems - A Survey. - Mingsheng Ying; Yuan Feng 001 (CoRR, 2018)

Decomposition of quantum Markov chains and its applications. - Ji Guan 001; Yuan Feng 001; Mingsheng Ying (J. Comput. Syst. Sci., 2018)

Super-activating quantum memory with entanglement. - Ji Guan 001; Yuan Feng 001; Mingsheng Ying (Quantum Inf. Comput., 2018)

Model Checking Applied to Quantum Physics. - Ji Guan 001; Yuan Feng 001; Andrea Turrini; Mingsheng Ying (CoRR, 2019)

A Monte Carlo Tree Search Framework for Quantum Circuit Transformation. - Xiangzhen Zhou; Yuan Feng 001; Sanjiang Li (ICCAD, 2020)

Quantum Hoare logic with classical variables. - Yuan Feng 001; Mingsheng Ying (CoRR, 2020)

Quantum Circuit Transformation Based on Simulated Annealing and Heuristic Search. - Xiangzhen Zhou; Sanjiang Li; Yuan Feng 001 (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2020)

Approximate Equivalence Checking of Noisy Quantum Circuits. - Xin Hong; Mingsheng Ying; Yuan Feng 001; Xiangzhen Zhou; Sanjiang Li (DAC, 2021)

Measuring the constrained reachability in quantum Markov chains. - Ming Xu 010; Cheng-Chao Huang; Yuan Feng 001 (Acta Informatica, 2021)

Optimal Policies for Quantum Markov Decision Processes. - Mingsheng Ying; Yuan Feng 001; Shenggang Ying (Int. J. Autom. Comput., 2021)

Symbolic Reasoning About Quantum Circuits in Coq. - Wenjun Shi; Qinxiang Cao; Yuxin Deng; Hanru Jiang; Yuan Feng 001 (J. Comput. Sci. Technol., 2021)

Qubit Mapping Based on Subgraph Isomorphism and Filtered Depth-Limited Search. - Sanjiang Li; Xiangzhen Zhou; Yuan Feng 001 (IEEE Trans. Computers, 2021)

Equivalence Checking of Dynamic Quantum Circuits. - Xin Hong; Yuan Feng 001; Sanjiang Li; Mingsheng Ying (ICCAD, 2022)

Formal semantics of a classical-quantum language. - Yuxin Deng; Yuan Feng 001 (Theor. Comput. Sci., 2022)

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

Verification of Distributed Quantum Programs. - Yuan Feng 001; Sanjiang Li; Mingsheng Ying (ACM Trans. Comput. Log., 2022)

A Tensor Network based Decision Diagram for Representation of Quantum Circuits. - Xin Hong; Xiangzhen Zhou; Sanjiang Li; Yuan Feng 001; Mingsheng Ying (ACM Trans. Design Autom. Electr. Syst., 2022)

Quantum Circuit Transformation: A Monte Carlo Tree Search Framework. - Xiangzhen Zhou; Yuan Feng 001; Sanjiang Li (ACM Trans. Design Autom. Electr. Syst., 2022)

Alternating Layered Variational Quantum Circuits Can Be Classically Optimized Efficiently Using Classical Shadows. - Afrad Basheer; Yuan Feng 001; Christopher Ferrie; Sanjiang Li (AAAI, 2023)

Two Views of Constrained Differential Privacy: Belief Revision and Update. - Likang Liu; Keke Sun; Chunlai Zhou; Yuan Feng 001 (AAAI, 2023)

Verification of Nondeterministic Quantum Programs. - Yuan Feng 001; Yingte Xu (ASPLOS (3), 2023)

Single-Qubit Gates Matter for Optimising Quantum Circuit Depth in Qubit Mapping. - Sanjiang Li; Ky Dan Nguyen; Zachary Clare; Yuan Feng 001 (ICCAD, 2023)

Decision Diagrams for Symbolic Verification of Quantum Circuits. - Xin Hong; Wei-Jia Huang; Wei-Chen Chien; Yuan Feng 001; Min-Hsiu Hsieh; Sanjiang Li; Chia-Shun Yeh; Mingsheng Ying (QCE, 2023)

Towards General Loop Invariant Generation via Coordinating Symbolic Execution and Large Language Models. - Chang Liu 021; Xiwei Wu; Yuan Feng 001; Qinxiang Cao; Junchi Yan (CoRR, 2023)

Refinement calculus of quantum programs with projective assertions. - Yuan Feng 001; Li Zhou 013; Yingte Xu (CoRR, 2023)

Supervised Learning Enhanced Quantum Circuit Transformation. - Xiangzhen Zhou; Yuan Feng 001; Sanjiang Li (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2023)

Model Checking for Probabilistic Multiagent Systems. - Chen Fu; Andrea Turrini; Xiaowei Huang 001; Lei Song 001; Yuan Feng 001; Lijun Zhang 001 (J. Comput. Sci. Technol., 2023)

Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs. - Yuan Feng 001; Sanjiang Li (Inf. Comput., 2023)

Measurement-Based Verification of Quantum Markov Chains. - Ji Guan 001; Yuan Feng 001; Andrea Turrini; Mingsheng Ying (CAV (3), 2024)

Ansatz-Agnostic Exponential Resource Saving in Variational Quantum Algorithms Using Shallow Shadows. - Afrad Basheer; Yuan Feng 001; Christopher Ferrie; Sanjiang Li (IJCAI, 2024)

Towards General Loop Invariant Generation: A Benchmark of Programs with Memory Manipulation. - Chang Liu 021; Xiwei Wu; Yuan Feng 001; Qinxiang Cao; Junchi Yan (NeurIPS, 2024)

Dynamic Transitive Closure-based Static Analysis through the Lens of Quantum Search. - Jiawei Ren 003; Yulei Sui; Xiao Cheng 002; Yuan Feng 001; Jianjun Zhao 001 (ACM Trans. Softw. Eng. Methodol., 2024)

On the Trainability and Classical Simulability of Learning Matrix Product States Variationally. - Afrad Basheer; Yuan Feng 001; Christopher Ferrie; Sanjiang Li; Hakop Pashayan (AAAI, 2025)

TrustGeoGen: Scalable and Formal-Verified Data Engine for Trustworthy Multi-modal Geometric Problem Solving. - Daocheng Fu; Zijun Chen; Renqiu Xia; Qi Liu; Yuan Feng 001; Hongbin Zhou; Renrui Zhang; Shiyang Feng; Peng Gao 007; Junchi Yan; Botian Shi; Bo Zhang 069; et al. (CoRR, 2025)