Developing formal methods and automatic tools for verification of quantum programs and cryptographic protocols.
Source: Wallpaper Flare
Quantum programming theory
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.
Program Leader: Prof Yuan Feng
Key Members: Prof Mingsheng Ying and Dr Yuval Sanders
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.
Tool support
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.
Selected research outputs
- M. Ying and Y. Feng. Model Checking Quantum Systems: Principles and Algorithms. Cambridge University Press, 2021.
- Y. Feng, S. Li, and M. Ying. Verification of Distributed Quantum Programs. ACM Transactions on Computational Logic 23(3), 19:1-19:40 (2022).
- X. Hong, X. Zhou, S. Li, Y. Feng, and M. Ying. A Tensor Network based Decision Diagram for Representation of Quantum Circuits. ACM Transactions on Design Automation of Electronic Systems 27 (6) 60:1-60:30 (2022).
- M. Ying, L. Zhou, Y. Li, Y. Feng. A proof system for disjoint parallel quantum programs. Theoretical Computer Science 897: 164-184 (2022).
- Y. Deng and Y. Feng. Formal Semantics of a Classical-Quantum Language. Theoretical Computer Science 913: 73-93 (2022).
- Y. Feng and M. Ying. Quantum Hoare logic with classical variables, ACM Transactions on Quantum Computing 2(4), 16:1-16:43 (2021).
- Y. Feng and Y. Xu. Verification of nondeterministic quantum programs. Proceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS’23) (2023).
- X. Hong, Y. Feng, S. Li, and M. Ying. Equivalence Checking of Dynamic Quantum Circuits. Proceedings of the 41st International Conference on Computer-Aided Design (ICCAD’22), 127:1-127:8 (2022).
- X. Hong, X. Zhou, S. Li, Y. Feng, and M. Ying. Approximate Equivalence Checking of Noisy Quantum Circuits. Proceedings of the 58th Design Automation Conference (DAC’21), 637-642 (2021).