Pith. sign in

REVIEW 1 cited by

Verification Logics for Quantum Programs

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

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

arxiv 1904.04304 v1 pith:346ALZLP submitted 2019-04-08 cs.LO cs.ETcs.PL

Robert Rand This is my paper · ORCID
classification cs.LOcs.ETcs.PL
keywords programsquantumlogicslanguageslogicverificationalgorithmassertions
verification ladder T0 review T1 audit T2 compute T3 formal
0 comments
read the original abstract

We survey the landscape of Hoare logics for quantum programs. We review three papers: "Reasoning about imperative quantum programs" by Chadha, Mateus and Sernadas; "A logic for formal verification of quantum programs" by Yoshihiko Kakutani; and "Floyd-hoare logic for quantum programs" by Mingsheng Ying. We compare the mathematical foundations of the logics, their underlying languages, and the expressivity of their assertions. We also use the languages to verify the Deutsch-Jozsa Algorithm, and discuss their relative usability in practice.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Noise-aware Verification and Synthesis of Quantum Programs

    cs.PL 2026-08 conditional novelty 6.0 of 10

    A noise-aware quantum Hoare logic and an automated synthesis method produce hardware-specific optimal quantum subroutines, showing that classical probabilistic branching can be necessary for optimality.

Pith tools