Reachability and Termination Analysis of Concurrent Quantum Programs. - Nengkun Yu; Mingsheng Ying (CONCUR, 2012)

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

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)

Determinantal Complexities and Field Extensions. - Youming Qiao; Xiaoming Sun 001; Nengkun Yu (ISAAC, 2013)

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

Orbit Problem Revisited - Taolue Chen 001; Xiaoming Sun 001; Nengkun Yu (CoRR, 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)

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

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

Distinguishability of Quantum States by Positive Operator-Valued Measures With Positive Partial Transpose. - Nengkun Yu; Runyao Duan; Mingsheng Ying (IEEE Trans. Inf. Theory, 2014)

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

Continuous-time orbit problems are decidable in polynomial-time. - Taolue Chen 001; Nengkun Yu; Tingting Han 001 (Inf. Process. Lett., 2015)

Limitations on Separable Measurements by Convex Optimization. - Somshubhro Bandyopadhyay; Alessandro Cosentino; Nathaniel Johnston; Vincent Russo; John Watrous; Nengkun Yu (IEEE Trans. Inf. Theory, 2015)

Quantum capacities for entanglement networks. - Shawn X. Cui; Zheng-Feng Ji; Nengkun Yu; Bei Zeng (ISIT, 2016)

Exponential separation of quantum communication and classical information. - Anurag Anshu; Dave Touchette; Penghui Yao; Nengkun Yu (STOC, 2017)

Sample-Optimal Tomography of Quantum States. - Jeongwan Haah; Aram W. Harrow; Zhengfeng Ji; Xiaodi Wu 001; Nengkun Yu (IEEE Trans. Inf. Theory, 2017)

Bounds on the Distance Between a Unital Quantum Channel and the Convex Hull of Unitary Channels. - Nengkun Yu; Runyao Duan; Quanhua Xu (IEEE Trans. Inf. Theory, 2017)

Capacity approaching coding for low noise interactive quantum communication. - Debbie W. Leung; Ashwin Nayak 001; Ala Shayeghi; Dave Touchette; Penghui Yao; Nengkun Yu (STOC, 2018)

Quantum Coupling and Strassen Theorem. - Li Zhou 013; Shenggang Ying; Nengkun Yu; Mingsheng Ying (CoRR, 2018)

An applied quantum Hoare logic. - Li Zhou 013; Nengkun Yu; Mingsheng Ying (PLDI, 2019)

Coupling Techniques for Reasoning about Quantum Programs. - Gilles Barthe; Justin Hsu; Mingsheng Ying; Nengkun Yu; Li Zhou 013 (CoRR, 2019)

Protocols for Packet Quantum Network Intercommunication. - Nengkun Yu; Ching-Yi Lai; Li Zhou 013 (CoRR, 2019)

Quantum Temporal Logic. - Nengkun Yu (CoRR, 2019)

Poq: Projection-based Runtime Assertions for Debugging on a Quantum Computer. - Gushu Li; Li Zhou 013; Nengkun Yu; Yufei Ding 001; Mingsheng Ying; Yuan Xie 001 (CoRR, 2019)

Verification of Continuous-time Markov Chains. - Ji Guan 001; Nengkun Yu (CoRR, 2020)

Local Equivalence of Multipartite Entanglement. - Youming Qiao; Xiaoming Sun 001; Nengkun Yu (IEEE J. Sel. Areas Commun., 2020)

Relational proofs for quantum programs. - Gilles Barthe; Justin Hsu; Mingsheng Ying; Nengkun Yu; Li Zhou 013 (Proc. ACM Program. Lang., 2020)

Projection-based runtime assertions for testing and debugging Quantum programs. - Gushu Li; Li Zhou 013; Nengkun Yu; Yufei Ding 001; Mingsheng Ying; Yuan Xie 001 (Proc. ACM Program. Lang., 2020)

Strassen's theorem for quantum couplings. - Li Zhou 013; Shenggang Ying; Nengkun Yu; Mingsheng Ying (Theor. Comput. Sci., 2020)

Multipartite Entanglement Certification, With or Without Tomography. - Nengkun Yu (IEEE Trans. Inf. Theory, 2020)

Model Checking Quantum Continuous-Time Markov Chains. - Ming Xu 010; Jingyi Mei; Ji Guan 001; Nengkun Yu (CONCUR, 2021)

Sample Efficient Identity Testing and Independence Testing of Quantum States. - Nengkun Yu (ITCS, 2021)

Discrimination of quantum states under locality constraints in the many-copy setting. - Hao-Chung Cheng; Andreas J. Winter 002; Nengkun Yu (ISIT, 2021)

A Quantum Interpretation of Bunched Logic & Quantum Separation Logic. - Li Zhou 013; Gilles Barthe; Justin Hsu; Mingsheng Ying; Nengkun Yu (LICS, 2021)

Quantum abstract interpretation. - Nengkun Yu; Jens Palsberg (PLDI, 2021)

Quantum Max-Flow Min-Cut theorem. - Nengkun Yu (CoRR, 2021)

Capacity Approaching Coding for Low Noise Interactive Quantum Communication Part I: Large Alphabets. - Debbie W. Leung; Ashwin Nayak 001; Ala Shayeghi; Dave Touchette; Penghui Yao; Nengkun Yu (IEEE Trans. Inf. Theory, 2021)

When is the Chernoff Exponent for Quantum Operations Finite? - Nengkun Yu; Li Zhou 013 (IEEE Trans. Inf. Theory, 2021)

Towards Efficient Reasoning of Quantum Programs. - Nengkun Yu (SAS, 2022)

A Probabilistic Logic for Verifying Continuous-time Markov Chains. - Ji Guan 001; Nengkun Yu (TACAS (2), 2022)

Checking Continuous Stochastic Logic against Quantum Continuous-Time Markov Chains. - Jingyi Mei; Ming Xu 010; Ji Guan 001; Yuxin Deng; Nengkun Yu (CoRR, 2022)

The QQUIC Transport Protocol: Quantum-Assisted UDP Internet Connections. - Peng Yan; Nengkun Yu (Entropy, 2022)

On incorrectness logic for Quantum programs. - Peng Yan; Hanru Jiang; Nengkun Yu (Proc. ACM Program. Lang., 2022)

Comments on and Corrections to "When Is the Chernoff Exponent for Quantum Operations Finite?". - Nengkun Yu; Li Zhou 013 (IEEE Trans. Inf. Theory, 2022)

Accelerating Voting by Quantum Computation. - Ao Liu 001; Qishen Han; Lirong Xia; Nengkun Yu (UAI, 2023)

Accelerating Majority Voting by Quantum Computation. - Ao Liu 001; Lirong Xia; Nengkun Yu (CoRR, 2023)

Structured Theorem for Quantum Programs and its Applications. - Nengkun Yu (ACM Trans. Softw. Eng. Methodol., 2023)

Almost Tight Sample Complexity Analysis of Quantum Identity Testing by Pauli Measurements. - Nengkun Yu (IEEE Trans. Inf. Theory, 2023)

Approximate Relational Reasoning for Quantum Programs. - Peng Yan; Hanru Jiang; Nengkun Yu (CAV (3), 2024)

Quantum temporal logic and reachability problems of matrix semigroups. - Nengkun Yu (Inf. Comput., 2024)

Pauli Measurements Are Not Optimal for Single-Copy Tomography. - Jayadev Acharya; Abhilash Dharmavarapu; Yuhan Liu; Nengkun Yu (STOC, 2025)

Scalable Equivalence Checking and Verification of Shallow Quantum Circuits. - Nengkun Yu; Xuan Du Trinh; Thomas Reps (CoRR, 2025)

Tight Bound for Quantum Unitary Time-Reversal. - Kean Chen; Nengkun Yu; Zhicheng Zhang (CoRR, 2025)

SAQR-QC: A Logic for Scalable but Approximate Quantitative Reasoning about Quantum Circuits. - Nengkun Yu; Jens Palsberg; Thomas Reps (CoRR, 2025)

Pauli Measurements Are Near-Optimal for Single-Qubit Tomography. - Jayadev Acharya; Abhilash Dharmavarapu; Yuhan Liu; Nengkun Yu (CoRR, 2025)

The Quantum Repeater Network Saturates the Entanglement Distribution Asymptotically. - Nengkun Yu (IEEE Trans. Inf. Theory, 2025)

Optimal Tomography of Quantum Markov Chains via Continuity of Petz Recovery States. - Li Gao; Nengkun Yu (IEEE Trans. Inf. Theory, 2025)