Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs

• URL: http://arxiv.org/abs/2206.13772v1
• Date: Tue, 28 Jun 2022 05:49:55 GMT
• Title: Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs
• Authors: Yuan Feng and Sanjiang Li
• Abstract summary: Hoare logic, and incorrectness (or reverse Hoare) logic are powerful techniques for static analysis of computer programs. We show that any complete quantum abstract interpretation induces a quantum Hoare logic and a quantum incorrectness logic.
• Score: 6.2147758224415055
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Abstract interpretation, Hoare logic, and incorrectness (or reverse Hoare) logic are powerful techniques for static analysis of computer programs. All of them have been successfully extended to the quantum setting, but largely developed in parallel. In this paper, we examine the relationship between these techniques in the context of verifying quantum while-programs, where the abstract domain and the set of assertions for quantum states are well-structured. In particular, we show that any complete quantum abstract interpretation induces a quantum Hoare logic and a quantum incorrectness logic, both of which are sound and relatively complete. Unlike the logics proposed in the literature, the induced logic systems are in a forward manner, making them more useful in certain applications. Conversely, any sound and relatively complete quantum Hoare logic or quantum incorrectness logic induces a complete quantum abstract interpretation. As an application, we are able to show the non-existence of any sound and relatively complete quantum Hoare logic or incorrectness logic if tuples of local subspaces are taken as assertions.

Related papers

• BI-based Reasoning about Quantum Programs with Heap Manipulations [5.744265100221585]
  We provide well-founded semantics for a quantum programming language Qwhile-hp with heap manipulations. We develop a quantum BI-style logic that includes interpretations for separating implication. We then adopt this quantum BI-style logic as an assertion language to reason about heap-manipulated quantum programs.
  arXiv  Detail & Related papers  (2024-09-16T10:34:45Z)
• Quantum algorithms: A survey of applications and end-to-end complexities [90.05272647148196]
  The anticipated applications of quantum computers span across science and industry. We present a survey of several potential application areas of quantum algorithms. We outline the challenges and opportunities in each area in an "end-to-end" fashion.
  arXiv  Detail & Related papers  (2023-10-04T17:53:55Z)
• Quantum process tomography of continuous-variable gates using coherent states [49.299443295581064]
  We demonstrate the use of coherent-state quantum process tomography (csQPT) for a bosonic-mode superconducting circuit. We show results for this method by characterizing a logical quantum gate constructed using displacement and SNAP operations on an encoded qubit.
  arXiv  Detail & Related papers  (2023-03-02T18:08:08Z)
• Birkhoff-von Neumann Quantum Logic as an Assertion Language for Quantum Programs [1.1878820609988696]
  A first-order logic with quantum variables is needed as an assertion language for specifying and reasoning about various properties of quantum programs. In this paper, we introduce a first-order extension of Birkhoff-von Neumann quantum logic with universal and existential quantifiers over quantum variables.
  arXiv  Detail & Related papers  (2022-05-04T08:57:44Z)
• LQP: The Dynamic Logic of Quantum Information [77.34726150561087]
  This paper introduces a dynamic logic formalism for reasoning about information flow in composite quantum systems. We present a finitary syntax, a relational semantics and a sound proof system for this logic. As applications, we use our system to give formal correctness for the Teleportation protocol and for a standard Quantum Secret Sharing protocol.
  arXiv  Detail & Related papers  (2021-10-04T12:20:23Z)
• The Logic of Quantum Programs [77.34726150561087]
  We present a logical calculus for reasoning about information flow in quantum programs. In particular we introduce a dynamic logic that is capable of dealing with quantum measurements, unitary evolutions and entanglements in compound quantum systems.
  arXiv  Detail & Related papers  (2021-09-14T16:08:37Z)
• Depth-efficient proofs of quantumness [77.34726150561087]
  A proof of quantumness is a type of challenge-response protocol in which a classical verifier can efficiently certify quantum advantage of an untrusted prover. In this paper, we give two proof of quantumness constructions in which the prover need only perform constant-depth quantum circuits.
  arXiv  Detail & Related papers  (2021-07-05T17:45:41Z)
• A Quantum Interpretation of Bunched Logic for Quantum Separation Logic [22.507329566323982]
  We develop a program logic where pre- and post-conditions are BI formulas describing quantum states. We exercise the logic for proving the security of quantum one-time pad and secret sharing.
  arXiv  Detail & Related papers  (2021-01-30T22:24:36Z)
• Quantum Hoare logic with classical variables [3.1181601933418897]
  We propose a quantum Hoare logic for a simple while language which involves both classical and quantum variables. With novel definitions of classical-quantum states and corresponding assertions, the logic system is quite simple and similar to the traditional Hoare logic for classical programs.
  arXiv  Detail & Related papers  (2020-08-15T23:56:18Z)
• Operational Resource Theory of Imaginarity [48.7576911714538]
  We show that quantum states are easier to create and manipulate if they only have real elements. As an application, we show that imaginarity plays a crucial role for state discrimination.
  arXiv  Detail & Related papers  (2020-07-29T14:03:38Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.