Formal Verification of Quantum Logic Circuits

本项目旨在为量子电路的形式建模、等效检验和模型检验提供全面的理论和有效的技术。随着量子计算硬件的快速发展，开发量子硬件设计和量子编译器的验证技术迫在眉睫。该项目中提出的算法和软件工具的成功开发将大大提高量子电路形式验证的知识，并帮助澳大利亚量子初创企业在迅速崛起的量子电子设计自动化（EDA）行业中建立并保持国际领先地位。

The project aims to develop comprehensive theory and effective techniques for formal modelling, equivalence checking, and model checking of quantum circuits. The research is timely as the rapid growth of quantum computing hardware makes it an urgent task to develop verification techniques for quantum hardware design and quantum compilers. The successful development of the algorithms and software tools proposed in this project will significantly advance the knowledge on formal verification of quantum circuits and help Australian quantum start-ups build and maintain an internationally leading position in the rapidly emerging quantum electronic design automation (EDA) industry.