Automated Expected Cost Analysis for Quantum Programs
This addresses the need for automated tool support in quantum programming, making cost analysis more accessible and efficient for developers, though it is incremental as it builds on existing frameworks.
The paper tackles the problem of automating expected cost analysis for quantum programs, which is tedious and error-prone manually, by presenting Qet, a static analysis tool that automatically infers precise upper bounds on expected costs for mixed classical-quantum programs with advanced features.
In recent years, quantum computing has gained a substantial amount of momentum, and the capabilities of quantum devices are continually expanding and improving. Nevertheless, writing a quantum program from scratch remains tedious and error-prone work, showcasing the clear demand for automated tool support. We present Qet, a fully automated static program analysis tool that yields a precise expected cost analysis of mixed classical-quantum programs. Qet supports programs with advanced features like mid-circuit measurements and classical control flow. The methodology of our prototype implementation is based on a recently proposed quantum expectation transformer framework, generalising Dijkstra's predicate transformer and Hoare logic. The prototype implementation Qet is evaluated on a number of case studies taken from the literature and online references. Qet is able to fully automatically infer precise upper bounds on the expected costs that previously could only be derived by tedious manual calculations.