Towards Classical Software Verification using Quantum Computers

TL;DR

This paper investigates leveraging quantum computing to accelerate the formal verification of classical programs, aiming to detect common programming errors more efficiently.

Contribution

It introduces a quantum-based approach for program verification by translating errors into SAT instances and solving them with quantum algorithms, potentially offering polynomial speedup.

Findings

Quantum algorithms successfully identified common programming errors.

Testing on quantum devices demonstrated feasibility of the approach.

Potential for asymptotic polynomial speedup in verification tasks.

Abstract

We explore the possibility of accelerating the formal verification of classical programs with a quantum computer. A common source of security flaws stems from the existence of common programming errors like use after free, null-pointer dereference, or division by zero. To aid in the discovery of such errors, we try to verify that no such flaws exist. In our approach, for some code snippet and undesired behaviour, a SAT instance is generated, which is satisfiable precisely if the behavior is present in the code. It is in turn converted to an optimization problem, that is solved on a quantum computer. This approach holds the potential of an asymptotically polynomial speedup. Minimal examples of common errors, like out-of-bounds and overflows, but also synthetic instances with special properties, specific number of solutions, or structure, are tested with different solvers and tried on a quantum device. We use the near-standard Quantum Approximation Optimisation Algorithm, an application of the Grover algorithm, and the Quantum Singular Value Transformation to find the optimal solution, and with it a satisfying assignment.