Developing formal methods and automatic tools for verification of quantum programs and cryptographic protocols.
Programming methodologies and technologies are a central theme of computer science. Due to the essential differences between the nature of the classical world and that of the quantum world, today’s programming techniques are not suited to quantum computers. Furthermore, as human intuition is poorly adapted to the quantum world, design and implementation errors will creep into complex quantum software and cryptographic systems. Quantum programming and verification group at QSI investigates how to program a future quantum computer, and in particular, how quantum features such as superposition and entanglement can be fully exploited in the new programming models. This group also aims to develop formal methods and automatic tools for verification of quantum programs and cryptographic protocols.
Models of quantum programming
We aim at discovering new programming models that can properly exploit the unique power of quantum computers. One challenge in quantum programming research is to understand control flow of quantum programs, quantum recursion, and concurrency in quantum computation.
Verification of quantum programs
Programming is error prone. It will be even worse to program a quantum computer. We try to build a logical foundation for verification of quantum programs, and to develop a chain of verification techniques including model-checking quantum systems.
Based on our theoretical research, we are designing and implementing a set of automatic tools for verifying correctness of quantum programs and security of quantum cryptographic protocols, including model-checker for quantum Markov chains, theorem prover for quantum programs, and bisimulation checker and emulation tool for quantum communicating processes.
Barthe, G, Hsu, J, Ying, M, Yu, N & Zhou, L 2020, 'Relational proofs for quantum programs', Proceedings of the ACM on Programming Languages, vol. 4, no. POPL, pp. 1-29.View/Download from: Publisher's site
Barthe, G, Hsu, J, Ying, M, Yu, N & Zhou, L 2019, 'Coupling Techniques for Reasoning about Quantum Programs.', CoRR, vol. abs/1901.05184.
Fang, K, Wang, X, Tomamichel, M & Duan, R 2019, 'Non-Asymptotic Entanglement Distillation', IEEE TRANSACTIONS ON INFORMATION THEORY, vol. 65, no. 10, pp. 6454-6465.View/Download: UTS OPUS or Publisher's site
Hung, S-H, Hietala, K, Zhu, S, Ying, M, Hicks, M & Wu, X 2019, 'Quantitative robustness analysis of quantum programs', Proceedings of the ACM on Programming Languages, vol. 3, no. POPL, pp. 1-29.View/Download from: Publisher's site
Li, R, Wu, B, Ying, M, Sun, X & Yang, G 2020, 'Quantum Supremacy Circuit Simulation on Sunway TaihuLight', IEEE TRANSACTIONS ON PARALLEL AND DISTRIBUTED SYSTEMS, vol. 31, no. 4, pp. 805-816.View/Download from: Publisher's site
Li, G, Zhou, L, Yu, N, Ding, Y, Ying, M & Xie, Y 2019, 'Poq: Projection-based Runtime Assertions for Debugging on a Quantum Computer.', CoRR, vol. abs/1911.12855.
Liu, J, Zhan, B, Wang, S, Ying, S, Liu, T, Li, Y, Ying, M & Zhan, N 2019, 'Quantum Hoare Logic.', Archive of Formal Proofs, vol. 2019.
Liu, J, Zhou, L & Ying, M 2019, 'Expected Runtime of Quantum Programs.', CoRR, vol. abs/1911.12557.
Wang, X, Fang, K & Duan, R 2019, 'Semidefinite Programming Converse Bounds for Quantum Communication', IEEE Transactions on Information Theory, vol. 65, no. 4, pp. 2583-2592.View/Download: Publisher's site
Wang, Q, Liu, J & Ying, M 2019, 'Equivalence Checking of Quantum Finite-State Machines.', CoRR, vol. abs/1901.02173.
Wang, Q & Ying, M 2020, 'Quantum Random Access Stored-Program Machines.', CoRR, vol. abs/2003.03514.
Wang, Q & Ying, M 2019, 'Quantum Büchi Automata', CoRR, vol. abs/1804.08982.
Zhou, X, Li, S & Feng, Y 2020, 'Quantum Circuit Transformation Based on Simulated Annealing and Heuristic Search', IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems.View/Download: UTS OPUS or Publisher's site
Liu, J, Zhan, B, Wang, S, Ying, S, Liu, T, Li, Y, Ying, M & Zhan, N 2019, 'Formal Verification of Quantum Algorithms Using Quantum Hoare Logic', COMPUTER AIDED VERIFICATION, CAV 2019, PT II, 31st International Conference on Computer-Aided Verification (CAV), SPRINGER INTERNATIONAL PUBLISHING AG, New York, NY, pp. 187-207.View/Download from: Publisher's site
Zhou, L, Yu, N & Ying, M 2019, 'An applied quantum hoare logic', Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 1149-1162.View/Download from: Publisher's site