A Practical Specification Language for Automatic Quantum Program Verification (Technical Report)

TL;DR

This paper introduces a new set-based specification language and a linear-complexity automata translation algorithm that enables fully automatic, scalable verification of quantum programs.

Contribution

It presents an extended specification language and a novel translation method that significantly improves automation and scalability in quantum program verification.

Findings

Automata size scales linearly with qubits due to controlled construction.

Automated verification is feasible at larger scales than before.

Enhanced expressiveness without sacrificing efficiency.

Abstract

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.