A Practical Specification Language for Automatic Quantum Program Verification (Technical Report)
This work addresses the scalability bottleneck in automatic quantum program verification for researchers and practitioners, enabling verification at previously infeasible scales.
The paper introduces a specification language and translation algorithm that enables fully automatic Hoare-style verification of quantum programs with up to 30 qubits, achieving linear complexity in qubit count and avoiding exponential blow-up.
Hoare-style verification provides a principled foundation for reasoning about the correctness of quantum programs, but existing approaches do not allow fully automatic verification. While automata-based verification scales well when specifications are given directly as automata, prior frameworks incur exponential blow-up when translating high-level set-based assertions into automata, which severely limits practicality. We introduce an extended set-based specification language and a specification-to-automata translation algorithm whose complexity is linear in the number of qubits, enabled by controlled automaton construction and qubit reordering. The resulting compact automata enable fully automatic Hoare-style verification of fixed-qubit quantum programs at previously infeasible scales, while substantially improving expressiveness without compromising efficiency.