An automated deductive verification framework for circuit-building quantum programs

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

zbMATH Keywords

quantum circuitsdeductive verificationquantum programming

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