Towards quantum programs verification: from Quipper circuits to QPMC

DOI10.1007/978-3-319-40578-0_16MaRDI QIDQ3186602zbMATH OpenOpenAlexFDO

Authors Linda Anticoli, Carla Piazza, L. Taglialegne, Paolo Zuliani

Publication date 10 August 2016

Published in Reversible Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-40578-0_16

zbMATH Keywords

model checkingquantum circuitsquantum languages

Mathematics Subject Classification ID

Theory of programming languages (68N15) Networks and circuits as models of computation; circuit complexity (68Q06) Quantum algorithms and complexity in the theory of computing (68Q12) Specification and verification (program logics, model checking, etc.) (68Q60) Quantum computation (81P68)

Recommendations

• Toward automatic verification of quantum programs
• scientific article; zbMATH DE number 1612487
• A logic for formal verification of quantum programs
• An introduction to quantum programming in Quipper
• An automated deductive verification framework for circuit-building quantum programs

Cites work

• An introduction to quantum programming in Quipper
• scientific article; zbMATH DE number 1579275 (Why is no real title available?)
• Model checking quantum Markov chains
• Specification and verification of quantum protocols

Cited in

(16)

• An automated deductive verification framework for circuit-building quantum programs
• Verification of quantum computation: an overview of existing approaches
• Certified quantum computation in Isabelle/HOL
• \(\mathcal{Q}\)\textsc{wire} practice: formal verification of quantum circuits in Coq
• Shaded tangles for the design and verification of quantum programs (extended abstract)
• Towards large-scale functional verification of universal quantum circuits
• \textit{Re}\(\mathcal{Q}\)\textsc{wire}: reasoning about reversible quantum circuits
• Verifying the Steane code with Quantomatic
• Invariants of quantum programs: characterisations and generation
• Quantum symbolic execution
• Quantum encoding of dynamic directed graphs
• Formal verification of quantum algorithms using quantum Hoare logic
• Mirrors and memory in quantum automata
• \textsf{symQV}: automated symbolic verification of quantum programs
• Model Checking for Verification of Quantum Circuits
• Toward automatic verification of quantum programs

Describes a project that uses

Uses Software

• PRISM
• QPMC
• qGCL
• Quipper

This page was built for publication: Towards quantum programs verification: from Quipper circuits to QPMC

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