Model Checking
Image Computation for Quantum Transition Systems. X. Hong, D. Gao, Sanjiang Li, S. Ying, M. Ying. DATE 2025.
QReach: A Reachability Analysis Tool for Quantum Markov Chains. A. Dai, Mingsheng Ying. CAV 2024.
Model Checking Quantum Systems: Principles and Algorithms. M Ying, Y Feng. Cambridge University Press, 2021
Equivalence Checking and Verification
Approximation Methods for Simulation and Equivalence Checking of Noisy Quantum Circuits. M. Huang, J. Guan, W. Fang, Mingsheng Ying. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2025.
Efficient Formal Verification of Quantum Error Correcting Programs. Q. Huang, L. Zhou, W. Fang, M. Zhao, Mingsheng Ying. PLDI 2025.
LimTDD: A Compact Decision Diagram Integrating Tensor and Local Invertible Map Representations. X. Hong, A. Dai, D. Gao, Sanjiang Li, Z. Ji, M. Ying. arXiv:2504.01168, 2025.
Verification of Recursively Defined Quantum Circuits. Mingsheng Ying, Z. Zhang. arXiv:2404.05934, 2024.
Equivalence Checking of Parameterised Quantum Circuits. X. Hong, W. J. Huang, W. C. Chien, Y. Feng, M. H. Hsieh, Sanjiang Li, M. Ying. arXiv:2404.18456, 2024.
Decision Diagrams for Symbolic Verification of Quantum Circuits. Xin Hong, Wei-Jia Huang, Wei-Chen Chien, Yuan Feng, Min-Hsiu Hsieh, Sanjiang Li, Chia-Shun Yeh and Mingsheng Ying. IEEE International Conference on Quantum Computing and Engineering (QCE) 2023 (arXiv:2308.00440)
Verification of Nondeterministic Quantum Programs. Yuan Feng and Yingte Xu. ASPLOS (3) 2023: 789-805
Equivalence checking of dynamic quantum circuits. X Hong, Y Feng, S Li, M Ying. Proceedings of the 41th International Conference on Computer-Aided Design, 2022. arXiv preprint arXiv:2106.01658
A Tensor Network based Decision Diagram for Representation of Quantum Circuits. X Hong, X Zhou, S Li, Y Feng, M Ying. ACM Transactions on Design Automation of Electronic Systems, 27, 6, Article 60 (November 2022), 30 pages. arXiv:2009.02618 (2020)[code]
Verification of Distributed Quantum Programs. Y Feng, S Li, M Ying. ACM Transactions on Transactions on Computational Logic, 23 (3), 1-40, 2022. arxiv:2104.14796
Approximate Equivalence Checking of Noisy Quantum Circuits. X Hong, M Ying, Y Feng, X Zhou, S Li. DAC 2021: 637-642. arXiv:2103.11595(2021)[code]
Quantum Compilation
Advancing Quantum State Preparation Using Decision Diagram with Local Invertible Maps. X. Hong, A. Dai, C. Li, Sanjiang Li, S. Ying, M. Ying. arXiv:2507.17170, 2025.
Quantum State Preparation Based on LimTDD. X. Hong, C. Li, A. Dai, Sanjiang Li, S. Ying, M. Ying. ICCAD 2025.
Optimal Compilation Strategies for QFT Circuits in Neutral-Atom Quantum Computing. D. Gao, Y. Li, S. Ying, Sanjiang Li. Scientific Reports, 2025.
Qubit Mapping: The Adaptive Divide-and-Conquer Approach. Y. Huang, X. Zhou, F. Meng, Sanjiang Li. Quantum Information Processing, 2025.
Dasatom: A Divide-and-Shuttle Atom Approach to Quantum Circuit Transformation. Y. Huang, D. Gao, S. Ying, Sanjiang Li. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2025.
Benchmarking Quantum Circuit Transformation with QKNOB Circuits. Sanjiang Li, X. Zhou, Y. Feng. IEEE Transactions on Quantum Engineering, 2025.
Single-Qubit Gates Matter for Optimising Quantum Circuit Depth in Qubit Mapping. Sanjiang Li, Ky Dan Nguyen, Zachary Clare, Yuan Feng. ICCAD 2023. arxiv:2308.00876 [code]
Supervised Learning Enhanced Quantum Circuit Transformation. X Zhou, Y Feng, S Li. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 42(2): 437-447 (2023) https://arxiv.org/abs/2110.03057
Quantum Circuit Transformation: A Monte Carlo Tree Search Framework. X Zhou, Y Feng, S Li. ACM Transactions on Design Automation of Electronic Systems, 27, 6, Article 59 (November 2022), 27 pages. (This is a significant extension of our ICCAD'20 paper)
Qubit mapping based on subgraph isomorphism and filtered depth-limited search. S Li, X Zhou, Y Feng. IEEE Transactions on Computers, 70(11): 1777-1788 (2021) (arXiv:2004.07138) [code]
Quantum circuit transformation based on simulated annealing and heuristic search. X Zhou, S Li, Y Feng. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 39(12):4683-4694, 2020 (arXiv:1908.08853) [code]
A Monte Carlo tree search framework for quantum circuit transformation. X Zhou, Y Feng, S Li. Proceedings of the 39th International Conference on Computer-Aided Design, 1-7, 2020. (arXiv:2008.09331)[code]