Formal verification of quantum algorithms using quantum Hoare logic

DOI10.1007/978-3-030-25543-5_12OpenAlexW2957722170MaRDI QIDQ6154880FDOQ6154880

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)

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

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

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)

Cited In (7)

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

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)