An Automata-Based Framework for Verification and Bug Hunting in Quantum Circuits
summary
Introduces an automata-based verification engine that encodes sets of quantum states as tree automata and implements gate semantics as automata transformers over an algebraic representation (no floating-point). A prototype tool verifies a 40-qubit circuit with 141,527 gates in about ten minutes and finds injected bugs in circuits up to ~320 qubits (thousands of gates) where other tools fail, trading full functional equivalence for scalable non-equivalence/bug hunting and opening a practical bridge between automata theory and quantum circuit analysis.
AI-written summary · about
chapters (13)
- 0:00Introduction
- 0:45Quantum vs classical states
- 2:12Quantum gates and decision trees
- 3:14Verifying quantum circuits
- 4:41Hoare triples for quantum
- 5:44Tree languages for states
- 7:11Tree automata for states
- 9:19Implementing gates in automata
- 10:45Symbolic execution extension
- 11:06Empirical evaluation
- 12:14Bug hunting in circuits
- 13:37Summary and future
- 14:22Q&A
related talks
27mParameterized Verification of Quantum Circuits
29mEfficiently Verifying Quantum Programs with Few T Gates
19mShaking Up Quantum Simulators with Fuzzing and Rigour
22mEfficient Formal Verification of Quantum Error Correcting Programs
23mAutomating Quantum Hoare Logic with Automata (Work-In-Progress)
40mDemocratizing quantum formal verification: the path-sum way
17mQGAT: A Generate-and-Test Paradigm for Quantum Circuits
42mQuantum program analysis: Verification and Testing