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.

翻译：我们探索了利用量子计算机加速经典程序形式化验证的可能性。安全漏洞的常见根源在于普遍存在的编程错误，例如释放后使用（use after free）、空指针解引用（null-pointer dereference）以及除零错误（division by zero）。为帮助发现此类错误，我们尝试验证代码中不存在此类缺陷。在我们的方法中，针对某段代码片段及其不良行为，会生成一个SAT实例（可满足性问题实例），当且仅当该行为存在于代码中时，此SAT实例才是可满足的。随后，该SAT实例被转化为一个优化问题，并在量子计算机上求解。该方法具有渐进多项式加速的潜力。我们对常见错误的最小实例（如越界和溢出），以及具有特殊属性（如特定解的数量或结构）的合成实例，采用了不同的求解器进行测试，并在量子设备上进行了尝试。我们运用近乎标准的量子近似优化算法（Quantum Approximation Optimisation Algorithm）、Grover算法的一种应用，以及量子奇异值变换（Quantum Singular Value Transformation）来寻找最优解，并由此得到可满足赋值。