\textsf{symQV}: automated symbolic verification of quantum programs

DOI10.1007/978-3-031-27481-7_12MaRDI QIDQ6174534zbMATH OpenFDO

Authors Fabian Bauer-Marquart, Stefan Leue, Christian Schilling

Publication date 17 August 2023

Published in Formal Methods (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2212.02267

zbMATH Keywords

abstractionformal verificationquantum computingsymbolic execution

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Quantum computation (81P68)

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).

Recommendations

• An automated deductive verification framework for circuit-building quantum programs
• Towards quantum programs verification: from Quipper circuits to QPMC
• Toward automatic verification of quantum programs
• Quantum symbolic execution
• Fast equivalence-checking for quantum circuits

Cites work

• -complete decision procedures for satisfiability over the reals
• \(\mathcal{Q}\)\textsc{wire} practice: formal verification of quantum circuits in Coq
• \(Q|SI\rangle \): a quantum programming environment
• An automated deductive verification framework for circuit-building quantum programs
• dReal: an SMT solver for nonlinear theories over the reals
• Formal verification of quantum algorithms using quantum Hoare logic
• Handbook of model checking
• scientific article; zbMATH DE number 1579275 (Why is no real title available?)
• scientific article; zbMATH DE number 5899272 (Why is no real title available?)
• scientific article; zbMATH DE number 1256737 (Why is no real title available?)
• scientific article; zbMATH DE number 7699438 (Why is no real title available?)
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Isabelle/HOL. A proof assistant for higher-order logic
• Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer
• Some undecidable problems involving elementary functions of a real variable
• SpecRepair: Counter-Example Guided Safety Repair of Deep Neural Networks
• Toward the first quantum simulation with quantum speedup
• Towards large-scale functional verification of universal quantum circuits

Cited in

(5)

• Qsym over Sym is free
• Quantum symbolic execution
• A Theory of Cartesian Arrays (with Applications in Quantum Circuit Verification)
• Verification of quantum systems using barrier certificates
• Equivalence checking of quantum circuits by model counting

This page was built for publication: \textsf{symQV}: automated symbolic verification of quantum programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6174534)