Toward automatic verification of quantum programs

Publication Type:
Journal Article
Formal Aspects of Computing, 2019, 31 (1), pp. 3 - 25
Issue Date:
Filename Description Size
Ying2019_Article_TowardAutomaticVerificationOfQ.pdfPublished Version825.15 kB
Adobe PDF
Full metadata record
© 2018, British Computer Society. 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.
Please use this identifier to cite or link to this item: