Yu-Fang Chen

Our research group has developed the AutoQ Project: Automata-based Quantum Program Verification, a novel framework offering fresh perspectives on quantum program verification. AutoQ is founded on interpreting quantum states as binary decision trees and quantum gates as transformations on these trees. This perspective introduces unique advantages but also challenges: unlike in classical symbolic verification where binary decision diagrams (BDDs) encode sets of states, in quantum contexts, a BDD represents only a single state. Our approach employs tree automata to overcome this limitation, representing sets of quantum states for scalable and accurate symbolic quantum program analysis.

Project publications

• Verifying Repeat-until-Success Protocols using Automata (OOPSLA 2026) - Repeat-until-success quantum protocol verification
• An Automata-Based Framework for Verification and Bug Hunting in Quantum Circuits (PLDI 2023) and (QPL 2023), invited to submit as a CACM research highlights article - Basic Framework
• AutoQ: An Automata-Based Quantum Circuit Verifier (CAV 2023) - Tool + Symbolic extension
• Verifying Quantum Circuits with Level-Synchronized Tree Automata (POPL 2025) - A Tree automata model specialized for quantum verification
• AutoQ 2.0: From Verification of Quantum Circuits to Verification of Quantum Programs (TACAS 2025) - Quantum program
• Parameterized Verification of Quantum Circuits (POPL 2026) - Circuit family with an arbitrary number of qubits
• A Practical Specification Language for Automatic Quantum Program Verification (CAV 2026) - Specification Language
• A Theory of Cartesian Arrays with Applications in Quantum Circuit Verification (CADE 2023) - An attempt to develop SMT theory for quantum
• Accelerating Quantum Circuit Simulation with Symbolic Execution and Loop Summarization (ICCAD 2024) - MTBDD-based quantum circuit simulation + loop summarization