In this talk, I will present a novel perspective on quantum states and gates by interpreting a quantum state as a binary decision tree and a quantum gate as a transformation on this tree. This approach brings up an intriguing challenge: in classical verification, binary decision diagrams (BDDs) effectively encode sets of states, but in the quantum context, a BDD can represent only a single state. This raises the question: how can we extend this to encode a set of quantum states?

Our initial solution explores the use of tree automata, a standard method for representing sets of trees. Building on this concept, we have developed a framework for automated quantum program verification, which I will discuss in detail during the talk. This framework offers new insights into the verification process and could potentially enhance the scalability and accuracy of quantum program analysis.

References:

An Automata-Based Framework for Verification and Bug Hunting in Quantum Circuits (PLDI 2023) and (QPL 2023) (Basic Framework)

AutoQ: An Automata-Based Quantum Circuit Verifier (CAV 2023) (Tool + Symbolic extension)

Verifying Quantum Circuits with Level-Synchronized Tree Automata (conditional accept, POPL 2025) (A Tree Automata Model Specialized for Quantum Verification)

AutoQ 2.0: From Verification of Quantum Circuits 2 to Verification of Quantum Programs (under submission) (Quantum Program)