symQV: Automated Symbolic Verification of Quantum Programs

Abstract

We present symQV, a symbolic execution framework for writing and verifying quantum computations in the quantum circuit model. symQV can automatically verify that a quantum program complies with a first-order specification. We formally introduce a symbolic quantum program model. This allows to encode the verification problem in an SMT formula, which can then be checked with a delta-complete decision procedure. We also propose an abstraction technique to speed up the verification process. Experimental results show that the abstraction improves symQV's scalability by an order of magnitude to quantum programs with 24 qubits (a 2^24-dimensional state space).

This is the extended version of a paper with the same title that appeared at FM 2023. Tool available at doi.org/10.5281/zenodo.7400321

References in corpus (5)

• A Quantum Approximate Optimization Algorithm
• Realizing Repeated Quantum Error Correction in a Distance-Three Surface Code
• Quantum Computing based Hybrid Solution Strategies for Large-scale Discrete-Continuous Optimization Problems
• Hybrid quantum convolutional neural networks model for COVID-19 prediction using chest X-Ray images
• Proving Quantum Programs Correct

Cited by in corpus (10)

• Symbolic Execution for Quantum Error Correction Programs
• Efficient Formal Verification of Quantum Error Correcting Programs
• A Case for Synthesis of Recursive Quantum Unitary Programs
• Verifying Fault-Tolerance of Quantum Error Correction Codes
• Automating Equational Proofs in Dirac Notation
• Automated Verification of Silq Quantum Programs using SMT Solvers
• Equivalence Checking of Quantum Circuits via Path-Sum and Weighted Model Counting
• A Practical Quantum Hoare Logic with Classical Variables, I
• Finding Photonics Circuits via $\delta$-weakening SMT
• Hybrid Path-Sums for Hybrid Quantum Programs