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

DOI10.1007/978-3-031-27481-7_12zbMath1529.68152arXiv2212.02267MaRDI QIDQ6174534

Stefan Leue, Fabian Bauer-Marquart, 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

formal verificationquantum computingabstractionsymbolic execution

Mathematics Subject Classification ID

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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
• An automated deductive verification framework for circuit-building quantum programs
• δ-Complete Decision Procedures for Satisfiability over the Reals
• Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer
• Handbook of Model Checking
• dReal: An SMT Solver for Nonlinear Theories over the Reals
• Toward the first quantum simulation with quantum speedup
• Some undecidable problems involving elementary functions of a real variable
• Formal verification of quantum algorithms using quantum Hoare logic
• \(Q|SI\rangle \): a quantum programming environment

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