Abstract: We present a new method for analyzing and identifying errors in quantum circuits. In our approach, we define the problem using a triple {P}C{Q}, where the task is to determine whether a given set P of quantum states at the input of a circuit C produces a set of quantum states at the output that is equal to, or included in, a set Q. We propose a technique that utilizes tree automata to represent sets of quantum states efficiently, and we develop algorithms to apply the operations of quantum gates within this representation. Our work creates a link between quantum program verification and automata, introducing new possibilities for leveraging automata theory and automata-based verification in the field of quantum computing. To enhance the effectiveness of this approach, we introduce a new model of tree automata called Level-synchronized tree automata (LSTAs), which extends classical tree automata by labeling each transition with a set of "choices" to synchronize subtrees of an accepted tree. This new model enables more efficient gate operations than classical tree automata. Additionally, we discuss our efforts to extend the framework from verifying quantum circuits to verifying quantum programs.
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.
*We strongly encourage attendees to use their full name (and if possible, their UMD credentials) to join the zoom session.*