An automated deductive verification framework for circuit-building quantum programs
From MaRDI portal
Publication:2233453
DOI10.1007/978-3-030-72019-3_6zbMath1473.68106arXiv2003.05841OpenAlexW3136504866MaRDI QIDQ2233453
Valentin Perrelle, Benoît Valiron, Sébastien Bardin, Christophe Chareton, François Bobot
Publication date: 18 October 2021
Full work available at URL: https://arxiv.org/abs/2003.05841
Quantum computation (81P68) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Quantum algorithms and complexity in the theory of computing (68Q12)
Related Items (5)
A strict constrained superposition calculus for graphs ⋮ \textsf{symQV}: automated symbolic verification of quantum programs ⋮ A formalization of the CHSH inequality and Tsirelson's upper-bound in Isabelle/HOL ⋮ The structure of sum-over-paths, its consequences, and completeness for Clifford ⋮ An automated deductive verification framework for circuit-building quantum programs
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- The spirit of ghost code
- Toward automatic verification of quantum programs
- Quantum implicit computational complexity
- REVS: a tool for space-optimized reversible circuit synthesis
- Verified compilation of space-efficient reversible circuits
- An automated deductive verification framework for circuit-building quantum programs
- Verification of quantum computation: an overview of existing approaches
- QPCF: higher-order languages and quantum circuits
- An Introduction to Quantum Programming in Quipper
- Model-Checking Linear-Time Properties of Quantum Systems
- Picturing Quantum Processes
- A Quantum Adiabatic Evolution Algorithm Applied to Random Instances of an NP-Complete Problem
- Quantomatic: A Proof Assistant for Diagrammatic Reasoning
- Quantum algorithms revisited
- How to Verify a Quantum Computation
- Why3 — Where Programs Meet Provers
- Invariants of quantum programs: characterisations and generation
- QWIRE: a core language for quantum circuits
- A lambda calculus for quantum computation with classical control
This page was built for publication: An automated deductive verification framework for circuit-building quantum programs
