We model quantum states as perfect binary trees and utilize tree automata to recognize large sets of such trees, allowing us to compactly represent collections of quantum states. Based on this novel approach, we design efficient algorithms for simulating quantum gates, enabling fast and scalable quantum circuit verification. Our method supports common quantum gates and control flow constructs.

Our research group is the first to solve quantum circuit verification with tree automata. On well-known circuits such as Bernstein-Vazirani and Grover's algorithm, our tool is much faster than existing tools, especially for the case of a large number of quantum states. Besides, the tool can be used to check the equivalence of two circuits and also support circuits with a variable number of qubits.

Our tool can be used to verify quantum circuit correctness before deployment and check circuit equivalence before and after compiler optimizations, supporting deployment platforms like IBM Qiskit. We can also develop an interactive, visual interface for quantum state preparation and gate operations like Frama-C. It can also be used to aid education by letting students compare circuits intuitively.