Join us in exploring cutting-edge research in formal methods, quantum programming, and automata theory. We welcome motivated Ph.D. students, postdocs, and collaborators.
Learn MoreOur 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.