pith. sign in

arxiv: 2404.18502 · v2 · submitted 2024-04-29 · 🪐 quant-ph · cs.CR· cs.ET

Towards Classical Software Verification using Quantum Computers

Sebastian Issel , Kilian Tscharke , Pascal Debus This is my paper

Pith reviewed 2026-05-24 02:22 UTC · model grok-4.3

classification 🪐 quant-ph cs.CRcs.ET
keywords quantum computingsoftware verificationSAT solvingQAOAformal verificationoptimizationGrover algorithm
0
0 comments X

The pith

Software verification for common errors can be mapped to optimization problems solvable by quantum algorithms with potential polynomial speedup.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper explores using quantum computers to verify classical programs against common errors by generating SAT instances that are satisfiable if the error exists. These instances are turned into optimization problems solved by quantum algorithms like QAOA, Grover, and QSVT. This method is demonstrated on small examples of errors such as out-of-bounds access and overflows, as well as synthetic cases. A reader would care because it suggests a way to make formal verification more efficient, potentially improving software security at scale.

Core claim

The authors establish that for a code snippet and an undesired behavior, a SAT instance can be generated that is satisfiable exactly when the behavior is present in the code; converting this to an optimization problem allows quantum computers to find a satisfying assignment using the Quantum Approximate Optimization Algorithm, an application of the Grover algorithm, and the Quantum Singular Value Transformation, with the potential of an asymptotically polynomial speedup.

What carries the argument

The pipeline that reduces program verification conditions to optimization problems solved on quantum hardware via QAOA and related quantum algorithms.

Load-bearing premise

That the optimization problems generated from realistic code verification instances can be solved efficiently by near-term quantum algorithms rather than requiring fully fault-tolerant quantum computers.

What would settle it

Demonstrating a realistic verification instance where the quantum optimization approach requires exponential resources or shows no advantage over classical SAT solvers would falsify the speedup claim.

Figures

Figures reproduced from arXiv: 2404.18502 by Kilian Tscharke, Pascal Debus, Sebastian Issel.

Figure 1
Figure 1. Figure 1: Convergence of QAOA and VQE for different solver and ansatz. [PITH_FULL_IMAGE:figures/full_fig_p010_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Convergence of RAO for different solver and ansatz. [PITH_FULL_IMAGE:figures/full_fig_p010_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: The used filters Fd,δ with different degree at δ = 1 10 . We see that a high degree is needed to amplify solutions, while also suppressing non-solutions. Smaller gaps would need even higher degree to be useful. To visualize how usable the approximation is, we introduce the following measure for a function f and gap δ. µf (δ) := |f(0)| 2 max ⌊δ−1⌋ j=1 |f(jδ)| 2 It measures how much a solution is amplified, … view at source ↗
Figure 4
Figure 4. Figure 4: Heatmap of the quality of the approximation for the gap [PITH_FULL_IMAGE:figures/full_fig_p013_4.png] view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The manuscript explores accelerating formal verification of classical programs by reducing checks for errors (e.g., use-after-free, null dereference) to SAT instances, mapping those to optimization problems (Ising form), and solving via QAOA, Grover, and QSVT on quantum hardware or simulators. It reports tests on minimal synthetic examples of out-of-bounds/overflow errors and instances with controlled solution counts or structure, while asserting potential for an asymptotically polynomial speedup.

Significance. If the mapping preserves quantum advantage and the speedup claim is substantiated with scaling analysis, the work would establish a concrete application domain for near-term quantum optimization in software security and formal methods. The reliance on standard, externally grounded reductions from program analysis to SAT to Ising is a methodological strength; however, the current lack of runtime data or scaling results prevents assessing whether this potential is realized beyond toy cases.

major comments (2)
  1. [Abstract] Abstract: the assertion that the approach 'holds the potential of an asymptotically polynomial speedup' is unsupported; no query-complexity derivation, gate-count analysis, or comparison (e.g., Grover O(sqrt(N)) versus CDCL scaling on verification-derived n-variable SAT instances) is provided anywhere in the manuscript.
  2. [Experimental evaluation] Experimental evaluation section: only 'minimal examples' and 'synthetic instances' are stated to have been tested with 'different solvers' and 'tried on a quantum device,' yet no quantitative metrics, success probabilities, iteration counts, or problem-size scaling data are reported, leaving the tractability assumption for realistic verification instances unexamined.
minor comments (2)
  1. [Approach] The description of the SAT-to-Ising conversion step would benefit from an explicit equation or pseudocode block showing how clauses are encoded into the objective function.
  2. [Figures/Tables] Figure captions and table headers (if present) should explicitly state the number of variables/clauses and the quantum backend used for each reported run.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the detailed and constructive report. We address each major comment below and indicate the revisions we will make.

read point-by-point responses

  1. Referee: [Abstract] Abstract: the assertion that the approach 'holds the potential of an asymptotically polynomial speedup' is unsupported; no query-complexity derivation, gate-count analysis, or comparison (e.g., Grover O(sqrt(N)) versus CDCL scaling on verification-derived n-variable SAT instances) is provided anywhere in the manuscript.

    Authors: We agree that the manuscript provides no explicit query-complexity derivation, gate-count analysis, or direct comparison against CDCL on verification-derived SAT instances. The phrase was intended to allude to the quadratic improvement possible with Grover search over unstructured enumeration, but we accept that this does not constitute a substantiated claim of asymptotic polynomial speedup. We will revise the abstract to remove the sentence and replace it with a more cautious statement that the approach maps verification to quantum optimization problems whose solution may benefit from known quantum speedups in search and optimization. revision: yes

  2. Referee: [Experimental evaluation] Experimental evaluation section: only 'minimal examples' and 'synthetic instances' are stated to have been tested with 'different solvers' and 'tried on a quantum device,' yet no quantitative metrics, success probabilities, iteration counts, or problem-size scaling data are reported, leaving the tractability assumption for realistic verification instances unexamined.

    Authors: The experimental section was deliberately limited to minimal synthetic cases to demonstrate that the SAT-to-Ising mapping is well-defined and that standard quantum algorithms can be applied. No claim is made about tractability on realistic verification instances, and the text does not assert that such instances are currently solvable. We will add the available quantitative data (success probabilities and iteration counts from the simulator runs) to the revised manuscript while explicitly stating that these results are illustrative only and that scaling behavior remains open. revision: partial

Circularity Check

0 steps flagged

No significant circularity; derivation relies on standard external reductions

full rationale

The manuscript describes a standard pipeline (program errors → SAT instance → Ising optimization) solved via QAOA/Grover/QSVT on minimal synthetic examples. No derivation step reduces a claimed result (such as the asserted potential for polynomial speedup) to its own inputs by construction, fitted parameters renamed as predictions, or load-bearing self-citations. The speedup statement is an unsupported assertion rather than a self-referential derivation, and the approach is externally grounded in known SAT-to-Ising mappings and quantum algorithms without circular reduction.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The paper relies on standard quantum computing primitives and classical reductions without introducing new fitted parameters or postulated entities.

axioms (1)
  • domain assumption Quantum algorithms (QAOA, Grover, QSVT) can be executed on available hardware or simulators to solve the generated optimization instances.
    Invoked when stating that the optimization problem is solved on a quantum computer.

pith-pipeline@v0.9.0 · 5712 in / 1039 out tokens · 20610 ms · 2026-05-24T02:22:27.061258+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

31 extracted references · 31 canonical work pages · 4 internal anchors

  1. [1]

    Control Flow Analysis

    Frances E. Allen. “Control Flow Analysis”. In:ACM SIGPLAN Notices 5.7 (July 1970), pp. 1–19.issn: 1558-1160. doi: 10/b6q4m9

    work page 1970

  2. [3]

    Quantum Random Access Codes with Shared Randomness

    doi: 10/grzghz. arXiv: 0810.2937. 14

    work page internal anchor Pith review Pith/arXiv arXiv

  3. [4]

    Barrett et al.Handbook of Satisfiability

    Clark W. Barrett et al.Handbook of Satisfiability. Ed. by Armin Biere. Frontiers in artificial intelligence and applications 0922-6389 v. 185. Master and use copy. Digital master created according to Benchmark for Faithful Digital Reproductions of Monographs and Serials, Version 1. Digital Li- brary Federation, December 2002. Amsterdam: IOS Press, 2011. 9...

    work page 2002

  4. [5]

    Software Model Checking: 20 Years And beyond

    Dirk Beyer and Andreas Podelski. “Software Model Checking: 20 Years And beyond”. In:Principles of Systems Design. Springer Nature Switzer- land, 2022, pp. 554–582.isbn: 9783031223372. doi: 10/gtpm9r

    work page 2022

  5. [6]

    Klee: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs

    Cristian Cadar, Daniel Dunbar, and Dawson Engler. “Klee: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs”. In:Proceedings of the 8th Usenix Conference on Operating Systems Design and Implementation. OSDI’08. San Diego, California: USENIX Association, 2008, pp. 209–224

    work page 2008

  6. [7]

    A Tool for Checking Ansi-C Programs

    Edmund Clarke, Daniel Kroening, and Flavio Lerda. “A Tool for Checking Ansi-C Programs”. In:Tools and Algorithms for the Construction and Analysis of Systems (tacas 2004). Ed. by Kurt Jensen and Andreas Podelski. Vol. 2988. Lecture Notes in Computer Science. Springer, 2004, pp. 168–176. isbn: 3-540-21299-X. url: https: // www .cs .cmu. edu/ ~svc/papers / ...

    work page 2004

  7. [8]

    Clarke et al.Model Checking

    Edmund M. Clarke et al.Model Checking. Second edition. The cyber- physical systems series. Cambridge, Massachusetts: The MIT Press, 2018. 402 pp.isbn: 978-0-262-03883-6.url: https://books.google.de/books? id=OJV5DwAAQBAJ

    work page 2018

  8. [9]

    Nickolas Davis et al.Software Verification Toolkit (svt): Survey on Available Software Verification Tools and Future Direction. Sept. 2022. doi: 10/ gtpm97

    work page 2022

  9. [10]

    A Quantum Approximate Optimization Algorithm

    Edward Farhi, Jeffrey Goldstone, and Sam Gutmann. “A Quantum Ap- proximate Optimization Algorithm”. In: (Nov. 14, 2014).doi: 10/g8n86t. arXiv: 1411.4028 [quant-ph]

    work page internal anchor Pith review Pith/arXiv arXiv 2014

  10. [11]

    Approximate Solutions of Combinatorial Problems Via Quantum Relaxations

    Bryce Fuller et al. “Approximate Solutions of Combinatorial Problems Via Quantum Relaxations”. In: (Nov. 4, 2021).doi: 10/grxrns. arXiv: 2111.03167 [quant-ph]

    work page arXiv 2021

  11. [12]

    Pysmt: A Solver-Agnostic Library for Fast Prototyping of Smt-Based Algorithms

    Marco Gario and Andrea Micheli. “Pysmt: A Solver-Agnostic Library for Fast Prototyping of Smt-Based Algorithms”. In:Smt Workshop 2015. 2015

    work page 2015

  12. [13]

    Quantum Singular Value Transformation & Its Algorith- mic Applications

    András Gilyén. “Quantum Singular Value Transformation & Its Algorith- mic Applications”. In: 2019.isbn: 9789402815092. url: https://api. semanticscholar.org/CorpusID:196183627

    work page 2019

  13. [14]

    A Fast Quantum Mechanical Algorithm for Database Search

    Lov K. Grover. “A Fast Quantum Mechanical Algorithm for Database Search”. In:Proceedings of the twenty-eighth annual ACM symposium on Theory of computing - STOC ’96. STOC ’96. ACM Press, 1996, pp. 212–

    work page 1996

  14. [15]

    The SeaHorn Verification Framework

    Arie Gurfinkel et al. “The SeaHorn Verification Framework”. In:Computer Aided Verification. Springer International Publishing, 2015, pp. 343–361. doi: 10/gf4cmd

    work page 2015

  15. [16]

    A User Study for Evaluation of For- mal Verification Results and Their Explanation at Bosch

    Arut Prakash Kaleeswaran et al. “A User Study for Evaluation of For- mal Verification Results and Their Explanation at Bosch”. In:Empirical Software Engineering28.5 (Sept. 2023).issn: 1573-7616. doi: 10/gtpnbk

    work page 2023

  16. [17]

    An Algorithmic Point of View

    Daniel Kroening and Ofer Strichman.Decision Procedures an Algorithmic Point of View. An Algorithmic Point of View. Springer Berlin / Heidelberg,

    work page

  17. [18]

    Optimal Polynomial Based Quantum Eigenstate Fil- tering with Application to Solving Quantum Linear Systems

    Lin Lin and Yu Tong. “Optimal Polynomial Based Quantum Eigenstate Fil- tering with Application to Solving Quantum Linear Systems”. In:Quantum 4, 361 (2020)4 (Oct. 31, 2019), p. 361.issn: 2521-327X. doi: 10/gtmtzg. arXiv: 1910.14596 [quant-ph]

    work page arXiv 2020

  18. [19]

    On the limited memory BFGS method for large scale optimization

    Dong C. Liu and Jorge Nocedal. “On the limited memory BFGS method for large scale optimization”. In:Mathematical Programming45.1–3 (Aug. 1989), pp. 503–528.issn: 1436-4646. doi: 10.1007/bf01589116

    work page doi:10.1007/bf01589116 1989

  19. [20]

    Ising formulations of many NP problems

    Andrew Lucas. “Ising Formulations of Many Np Problems”. In:Aip. Conf. Proc.2 (2014). issn: 2296-424X. doi: 10/gddjsh. arXiv: 1302.5843

    work page internal anchor Pith review Pith/arXiv arXiv 2014

  20. [21]

    A Survey on Compo- sitional Algorithms for Verification and Synthesis in Supervisory Control

    Robi Malik, Sahar Mohajerani, and Martin Fabian. “A Survey on Compo- sitional Algorithms for Verification and Synthesis in Supervisory Control”. In: Discrete Event Dynamic Systems33.3 (Aug. 2023), pp. 279–340.issn: 1573-7594. doi: 10/gsnjqn

    work page 2023

  21. [22]

    Grand Unification of Quantum Algorithms

    John M. Martyn et al. “Grand Unification of Quantum Algorithms”. In: PRX Quantum 2 (4 Dec. 2021), p. 040203.doi: 10/gnpx8n

    work page 2021

  22. [23]

    Z3: An Efficient Smt Solver

    Leonardo de Moura and Nikolaj Bjørner. “Z3: An Efficient Smt Solver”. In: 2008 Tools and Algorithms for Construction and Analysis of Systems. Springer, Berlin, Heidelberg, Mar. 2008, pp. 337–340.url: https : / / www.microsoft.com/en-us/research/publication/z3-an-efficient- smt-solver/

    work page 2008

  23. [24]

    Unitary $2$-designs from random $X$- and $Z$-diagonal unitaries

    YoshifumiNakataetal.“Unitary 2-DesignsfromRandom x-and z-Diagonal Unitaries”. In:J. Math. Phys. 58, 052203 (2017)58.5 (Feb. 26, 2015).issn: 1089-7658. doi: 10/gjs9rt. arXiv: 1502.07514 [quant-ph]

    work page internal anchor Pith review Pith/arXiv arXiv 2017

  24. [25]

    A Direct Search Optimization Method That Models the Objective and Constraint Functions by Linear Interpolation

    M. J. D. Powell. “A Direct Search Optimization Method That Models the Objective and Constraint Functions by Linear Interpolation”. In:Ad- vances in Optimization and Numerical Analysis. Springer Netherlands, 1994, pp. 51–67.isbn: 9789401583305. doi: 10/gft3s8

    work page 1994

  25. [26]

    Punnen, ed.The Quadratic Unconstrained Binary Optimiza- tion Problem

    Abraham P. Punnen, ed.The Quadratic Unconstrained Binary Optimiza- tion Problem. Springer International Publishing, 2022.doi: 10/gsjc23

    work page 2022

  26. [27]

    Classes of Recursively Enumerable Sets and Their Decision Problems

    H. G. Rice. “Classes of Recursively Enumerable Sets and Their Decision Problems”. In:Transactions of the American Mathematical Society74.2 (1953), pp. 358–366.issn: 1088-6850. doi: 10/bbxjqd. 16

    work page 1953

  27. [28]

    Unified Framework and Survey for Model Verifi- cation, Validation and Uncertainty Quantification

    Stefan Riedmaier et al. “Unified Framework and Survey for Model Verifi- cation, Validation and Uncertainty Quantification”. In:Archives of Com- putational Methods in Engineering28.4 (Aug. 2020), pp. 2655–2688.issn: 1886-1784. doi: 10/gtpm93

    work page 2020

  28. [29]

    An Overview of the Simultaneous Perturbation Method for Efficient Optimization

    James C. Spall. “An Overview of the Simultaneous Perturbation Method for Efficient Optimization”. In:Johns Hopkins Apl Technical Digest19 (1998), pp. 482–492.url: https : / / api . semanticscholar . org / CorpusID : 7988308

    work page 1998

  29. [30]

    A Cs Guide to the Quantum Singular Value Transformation

    Ewin Tang and Kevin Tian. “A Cs Guide to the Quantum Singular Value Transformation”. In: (Feb. 28, 2023).doi: 10/g8n8mq. arXiv: 2302.14324 [quant-ph]

    work page arXiv 2023

  30. [31]

    The Variational Quantum Eigensolver: A Review of Methods and Best Practices

    Jules Tilly et al. “The Variational Quantum Eigensolver: A Review of Methods and Best Practices”. In:Phys. Rep.986 (Nov. 9, 2021), pp. 1–128. doi: 10/grx7j3. arXiv: 2111.05176 [quant-ph]

    work page arXiv 2021

  31. [32]

    Model Checking for Verification of Quantum Circuits

    Mingsheng Ying. “Model Checking for Verification of Quantum Circuits”. In: (Apr. 23, 2021).doi: 10/gtpm94. arXiv: 2104.11359 [quant-ph]. 17 Table 1: Used examples of software errors and logical expressions. Name T est Case Out of Bounds i n t buf [1]; buf [1] = 0; Invalid Conversion short s = 1024; char c = ( char ) s ; Division by Zero f l o a t i = 1 / ...

    work page arXiv 2021