REVIEW 1 cited by
On the Relative Completeness of Satisfaction-based Quantum Hoare Logic
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
On the Relative Completeness of Satisfaction-based Quantum Hoare Logic
read the original abstract
Quantum Hoare logic (QHL) is a formal verification tool specifically designed to ensure the correctness of quantum programs. There has been an ongoing challenge to achieve a relatively complete satisfaction-based QHL with while-loop since its inception in 2006. This paper presents a solution by proposing the first relatively complete satisfaction-based QHL with while-loop. The completeness is proved in two steps. First, we establish a semantics and proof system of Hoare triples with quantum programs and deterministic assertions. Then, by utilizing the weakest precondition of deterministic assertion, we construct the weakest preterm calculus of probabilistic expressions. The relative completeness of QHL is then obtained as a consequence of the weakest preterm calculus. Using our QHL, we formally verify the correctness of Deutsch's algorithm and quantum teleportation.
Forward citations
Cited by 1 Pith paper
-
Formal Verification of Continuous-Variable Quantum Programs
A sound and relatively complete Hoare logic for continuous-variable quantum programs, with polynomial assertions and an automated weakest-precondition calculator.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.