\textsf{symQV}: automated symbolic verification of quantum programs
From MaRDI portal
Publication:6174534
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
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
