Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Towards Classical Software Verification using Quantum Computers

Sebastian Issel, Kilian Tscharke, Pascal Debus

TL;DR

The paper investigates accelerating formal verification of classical software using quantum computers by converting verification tasks into SAT, then into a QUBO, and solving with varied quantum approaches. It presents an end-to-end pipeline, including a SAT-to-QUBO mapping with a guaranteed gap, and a comparative study of VQA, Grover, and QSVT-based solvers, tested on real hardware and simulators. Hardware results show that while VQA/QAOA and RAO can be promising, hardware noise and encoding challenges currently limit practical gains, with Grover and QSVT facing even stiffer limitations. The work demonstrates feasibility and provides a roadmap for future improvements in encodings, error correction, and hardware-aware implementations to enable quantum-accelerated software verification. The approach offers a principled path to potentially faster verification of software properties, contingent on advances in quantum hardware and encoding techniques.

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.

Towards Classical Software Verification using Quantum Computers

TL;DR

The paper investigates accelerating formal verification of classical software using quantum computers by converting verification tasks into SAT, then into a QUBO, and solving with varied quantum approaches. It presents an end-to-end pipeline, including a SAT-to-QUBO mapping with a guaranteed gap, and a comparative study of VQA, Grover, and QSVT-based solvers, tested on real hardware and simulators. Hardware results show that while VQA/QAOA and RAO can be promising, hardware noise and encoding challenges currently limit practical gains, with Grover and QSVT facing even stiffer limitations. The work demonstrates feasibility and provides a roadmap for future improvements in encodings, error correction, and hardware-aware implementations to enable quantum-accelerated software verification. The approach offers a principled path to potentially faster verification of software properties, contingent on advances in quantum hardware and encoding techniques.

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.
Paper Structure (19 sections, 12 equations, 4 figures, 2 tables)

This paper contains 19 sections, 12 equations, 4 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Structure
  3. Related Work
  4. Generating a SAT instance
  5. Introduction to CNF-SAT
  6. Expressing the Existence of Errors as a Formula
  7. Generating the Optimization Problem
  8. Satisfiability as Optimum in a Quadratic Program
  9. Finding the Optimum
  10. VQA
  11. Grover
  12. Eigenvalue Filter by QSVT
  13. Test Cases
  14. Results
  15. VQA
  16. ...and 4 more sections

Figures (4)

  • Figure 1: Convergence of QAOA and VQE for different solver and ansatz.
  • Figure 2: Convergence of RAO for different solver and ansatz.
  • Figure 3: The used filters $F_{d,\delta}$ with different degree at $\delta=\frac{1}{10}$.
  • Figure 4: Heatmap of the quality of the approximation for the gap $\delta$ given by the y-axis with degree $d$ given by the x-axis, according to the explained measure $\mu_{F_{d,\delta}}(\delta)$.