Toward Automatic Verification of Quantum Programs
classification
🪐 quant-ph
cs.LO
keywords
quantumprogramslogicverificationanalysisapproachauthorautomatic
pith:TLROIBLU Add to your LaTeX paper
What is a Pith Number?\usepackage{pith}
\pithnumber{TLROIBLU}
Prints a linked pith:TLROIBLU badge after your title and writes the identifier into PDF metadata. Compiles on arXiv with no extra files. Learn more
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.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.