Verifying Quantum Circuits with Level-Synchronized Tree Automata

Explore a groundbreaking 20-minute conference talk from POPL 2025 that introduces a novel method for quantum circuit verification using level-synchronized tree automata (LSTAs). Learn how researchers from Uppsala University, Academia Sinica, Brno University of Technology, and other institutions have developed a symbolic representation of quantum states that offers significant advantages over traditional approaches. The presentation details how LSTAs extend classical tree automata while maintaining crucial properties like closure under union and intersection. Discover how this approach achieves quadratic complexity for gate operations—a dramatic improvement over previous exponential worst-case methods—and enables parameterized verification for families of circuits regardless of qubit count. The speakers demonstrate their C++ implementation that outperforms existing symbolic verifiers and simulators, handling problems orders of magnitude larger than current state-of-the-art solutions. This ACM SIGPLAN-sponsored talk includes references to the published article and supplementary materials that have earned "Artifacts Available" and "Artifacts Evaluated — Reusable" badges.