Toward Automatic Verification of Quantum Programs

Mingsheng Ying

REVIEW

Toward Automatic Verification of 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 1807.11610 v1 pith:TLROIBLU submitted 2018-07-31 quant-ph cs.LO

Toward Automatic Verification of Quantum Programs

Mingsheng Ying This is my paper

classification quant-ph cs.LO

keywords quantumprogramslogicverificationanalysisapproachauthorautomatic

verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

0 comments

read the original abstract

This paper summarises the results obtained by the author and his collaborators in a program logic approach to the verification of quantum programs, including quantum Hoare logic, invariant generation and termination analysis for quantum programs. It also introduces the notion of proof outline and several auxiliary rules for more conveniently reasoning about quantum programs. Some problems for future research are proposed at the end of the paper.

Toward Automatic Verification of Quantum Programs

discussion (0)