A logic for formal verification of quantum programs

DOI10.1007/978-3-642-10622-4_7MaRDI QIDQ3656843zbMATH OpenOpenAlexFDO

Authors Yoshihiko Kakutani

Publication date 14 January 2010

Published in Advances in Computer Science - ASIAN 2009. Information Security and Privacy (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-10622-4_7

Mathematics Subject Classification ID

Logic in computer science (03B70) 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
• Reasoning about imperative quantum programs
• Theoretical Aspects of Computing – ICTAC 2005
• DYNAMIC QUANTUM LOGIC FOR QUANTUM PROGRAMS

Cited in

(23)

• Reasoning about faulty quantum programs
• Deriving the correctness of quantum protocols in the probabilistic logic for quantum programs
• A proof system for disjoint parallel quantum programs
• Model checking for entanglement swapping
• Formal semantics of a classical-quantum language
• An automated deductive verification framework for circuit-building quantum programs
• Formal meta-level analysis framework for quantum programming languages
• Proof rules for the correctness of quantum programs
• Certified quantum computation in Isabelle/HOL
• Reasoning about imperative quantum programs
• Formal verification of optical quantum flip gate
• Towards quantum programs verification: from Quipper circuits to QPMC
• \(\mathcal{Q}\)\textsc{wire} practice: formal verification of quantum circuits in Coq
• Quantum Predicative Programming
• DYNAMIC QUANTUM LOGIC FOR QUANTUM PROGRAMS
• Verification of distributed quantum programs
• Theoretical Aspects of Computing – ICTAC 2005
• Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs
• Formal verification of quantum algorithms using quantum Hoare logic
• Quantum Hoare logic with ghost variables
• Toward automatic verification of quantum programs
• Quantum relational Hoare logic with expectations
• A dynamic logic for QASM programs

This page was built for publication: A logic for formal verification of quantum programs

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