Formal Verification of Quantum Logic Circuits

Project Member(s): Li, S., Feng, Y.

Funding or Partner Organisation: Australian Research Council (ARC Discovery Projects)
Australian Research Council (ARC Discovery Projects)

Start year: 2022

Summary: The rapid growth of quantum computing hardware makes it an urgent task to develop effective techniques for synthesis, optimisation, testing, and verification of quantum logic circuits. This project aims to develop comprehensive theory and effective techniques for formal modelling, equivalence checking, and model checking of quantum circuits, with applications for verifying 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 EDA industry.

FOR Codes: Expanding knowledge in the information and computing sciences, Application software packages, Computational logic and formal languages

Acknowledgement of Country

UTS acknowledges the Gadigal people of the Eora Nation, the Boorooberongal people of the Dharug Nation, the Bidiagal people and the Gamaygal people, upon whose ancestral lands our university stands. We would also like to pay respect to the Elders both past and present, acknowledging them as the traditional custodians of knowledge for these lands.