Toward automatic verification of quantum programs

Ying, M

Toward automatic verification of quantum programs

Ying, M

Permalink

Publication Type:: Journal Article
Citation:: Formal Aspects of Computing, 2019, 31 (1), pp. 3 - 25
Issue Date:: 2019-02-12

Closed Access

	Filename	Description	Size
	Ying2019_Article_TowardAutomaticVerificationOfQ.pdf	Published Version	825.15 kB	Adobe PDF	View/Open

Copyright Clearance Process

Recently Added
In Progress
Closed Access

This item is closed access and not available.

Full metadata record

Field	Value	Language
dc.contributor.author	Ying, M https://orcid.org/0000-0003-4847-702X	en_US
dc.date.issued	2019-02-12	en_US
dc.identifier.citation	Formal Aspects of Computing, 2019, 31 (1), pp. 3 - 25	en_US
dc.identifier.issn	0934-5043	en_US
dc.identifier.uri	http://hdl.handle.net/10453/131738
dc.description.abstract	© 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.	en_US
dc.relation	http://purl.org/au-research/grants/arc/DP160101652
dc.relation.ispartof	Formal Aspects of Computing	en_US
dc.relation.isbasedon	10.1007/s00165-018-0465-3	en_US
dc.subject.classification	Computation Theory & Mathematics	en_US
dc.title	Toward automatic verification of quantum programs	en_US
dc.type	Journal Article
utslib.citation.volume	1	en_US
utslib.citation.volume	31	en_US
utslib.for	0802 Computation Theory and Mathematics	en_US
utslib.for	0803 Computer Software	en_US
pubs.embargo.period	Not known	en_US
pubs.organisational-group	/University of Technology Sydney
pubs.organisational-group	/University of Technology Sydney/Faculty of Engineering and Information Technology
pubs.organisational-group	/University of Technology Sydney/Strength - QSI - Centre for Quantum Software and Information
utslib.copyright.status	closed_access
pubs.issue	1	en_US
pubs.publication-status	Published	en_US
pubs.volume	31	en_US

Abstract:

© 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:

http://hdl.handle.net/10453/131738