Formal verification of quantum algorithms using quantum Hoare logic

DOI10.1007/978-3-030-25543-5_12MaRDI QIDQ6154880zbMATH OpenOpenAlexFDO

Authors Junyi Liu, Bohua Zhan, Shu-Ling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying, Naijun Zhan

Publication date 16 February 2024

Published in Computer Aided Verification (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-25543-5_12

Mathematics Subject Classification ID

Quantum algorithms and complexity in the theory of computing (68Q12) Specification and verification (program logics, model checking, etc.) (68Q60) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• A logic for formal verification of quantum programs
• Toward automatic verification of quantum programs
• Certified quantum computation in Isabelle/HOL
• Theoretical Aspects of Computing – ICTAC 2005
• Towards quantum programs verification: from Quipper circuits to QPMC

Cited in

(8)

• Certified quantum computation in Isabelle/HOL
• Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs
• \textsf{symQV}: automated symbolic verification of quantum programs
• A formalization of the CHSH inequality and Tsirelson's upper-bound in Isabelle/HOL
• Verification of quantum systems using barrier certificates
• A Coq-based infrastructure for quantum programming, verification and simulation
• Quantum Hoare logic with ghost variables
• Formal reasoning about Bernstein-Vazirani algorithm

This page was built for publication: Formal verification of quantum algorithms using quantum Hoare logic

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