CS Talk
Yu-Fang Chen
Institute of Information Science, Academia Sinica
Host: Ruzica Piskac
Title: An automata-based approach for quantum circuit/program verification
Abstract:
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 to Verification of Quantum Programs (under submission) (Quantum Program)
Bio:
Yu-Fang Chen has been a Research Fellow/Professor at the Institute of Information Science, Academia Sinica, since 2015. His research primarily focuses on developing algorithms for formal verification, with a recent emphasis on automating quantum program verification. He has received several recent awards, including a Best Paper Nomination at TACAS 2024, Distinguished Paper Awards at OOPSLA 2023 and PLDI 2023, and a Best Paper Award at FM 2023. Over the past five years, Yu-Fang has actively contributed to the academic community by serving on the program committees of more than 30 international conferences, including top-tier events such as CAV 2022-2024, LICS 2021, CONCUR 2020, TACAS 2019, and ATVA 2019-2024. He was the Program Committee Co-Chair for ATVA 2019, and since 2021, he has been one of the five Steering Committee Members for ATVA.