Towards Classical Software Verification using Quantum Computers

• URL: http://arxiv.org/abs/2404.18502v1
• Date: Mon, 29 Apr 2024 08:43:58 GMT
• Title: Towards Classical Software Verification using Quantum Computers
• Authors: Sebastian Issel, Kilian Tscharke, Pascal Debus,
• Abstract summary: We explore the possibility of accelerating the formal verification of classical programs with a quantum computer. Minimal examples of common errors, like out-of-bounds and overflows, are tested with different solvers and tried on a quantum device.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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.

Related papers

• Quantum algorithms: A survey of applications and end-to-end complexities [90.05272647148196]
  The anticipated applications of quantum computers span across science and industry. We present a survey of several potential application areas of quantum algorithms. We outline the challenges and opportunities in each area in an "end-to-end" fashion.
  arXiv  Detail & Related papers  (2023-10-04T17:53:55Z)
• Enhancing Quantum Algorithms for Quadratic Unconstrained Binary Optimization via Integer Programming [0.0]
  In this work, we integrate the potentials of quantum and classical techniques for optimization. We reduce the problem size according to a linear relaxation such that the reduced problem can be handled by quantum machines of limited size. We present numerous computational results from real quantum hardware.
  arXiv  Detail & Related papers  (2023-02-10T20:12:53Z)
• Deep Quantum Error Correction [73.54643419792453]
  Quantum error correction codes (QECC) are a key component for realizing the potential of quantum computing. In this work, we efficiently train novel emphend-to-end deep quantum error decoders. The proposed method demonstrates the power of neural decoders for QECC by achieving state-of-the-art accuracy.
  arXiv  Detail & Related papers  (2023-01-27T08:16:26Z)
• Quantum Worst-Case to Average-Case Reductions for All Linear Problems [66.65497337069792]
  We study the problem of designing worst-case to average-case reductions for quantum algorithms. We provide an explicit and efficient transformation of quantum algorithms that are only correct on a small fraction of their inputs into ones that are correct on all inputs.
  arXiv  Detail & Related papers  (2022-12-06T22:01:49Z)
• A Quantum Algorithm for Computing All Diagnoses of a Switching Circuit [73.70667578066775]
  Faults are by nature while most man-made systems, and especially computers, work deterministically. This paper provides such a connecting via quantum information theory which is an intuitive approach as quantum physics obeys probability laws.
  arXiv  Detail & Related papers  (2022-09-08T17:55:30Z)
• Quantum Speedup for Higher-Order Unconstrained Binary Optimization and MIMO Maximum Likelihood Detection [2.5272389610447856]
  We propose a quantum algorithm that supports a real-valued higher-order unconstrained binary optimization problem. The proposed algorithm is capable of reducing the query complexity in the classical domain and providing a quadratic speedup in the quantum domain.
  arXiv  Detail & Related papers  (2022-05-31T00:14:49Z)
• Adiabatic Quantum Computing for Multi Object Tracking [170.8716555363907]
  Multi-Object Tracking (MOT) is most often approached in the tracking-by-detection paradigm, where object detections are associated through time. As these optimization problems are often NP-hard, they can only be solved exactly for small instances on current hardware. We show that our approach is competitive compared with state-of-the-art optimization-based approaches, even when using of-the-shelf integer programming solvers.
  arXiv  Detail & Related papers  (2022-02-17T18:59:20Z)
• A Hybrid Quantum-Classical Algorithm for Robust Fitting [47.42391857319388]
  We propose a hybrid quantum-classical algorithm for robust fitting. Our core contribution is a novel robust fitting formulation that solves a sequence of integer programs. We present results obtained using an actual quantum computer.
  arXiv  Detail & Related papers  (2022-01-25T05:59:24Z)
• Compilation of Fault-Tolerant Quantum Heuristics for Combinatorial Optimization [0.14755786263360526]
  We explore which quantum algorithms for optimization might be most practical to try out on a small fault-tolerant quantum computer. Our results discourage the notion that any quantum optimization realizing only a quadratic speedup will achieve an advantage over classical algorithms.
  arXiv  Detail & Related papers  (2020-07-14T22:54:04Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.