Verification of Quantum Programs

Feng, Y; Ying, MS

Verification of Quantum Programs

Feng, Y Ying, MS

Permalink

Publication Type:: Journal Article
Citation:: Ruan Jian Xue Bao/Journal of Software, 2018, 29, (4), pp. 1085-1093
Issue Date:: 2018-01-01

Closed Access

	Filename	Description	Size
	19429590_8592776020005671.pdf	Published version	2.34 MB	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	Feng, Y
dc.contributor.author	Ying, MS
dc.date.accessioned	2022-08-24T22:18:31Z
dc.date.available	2022-08-24T22:18:31Z
dc.date.issued	2018-01-01
dc.identifier.citation	Ruan Jian Xue Bao/Journal of Software, 2018, 29, (4), pp. 1085-1093
dc.identifier.issn	1000-9825
dc.identifier.uri	http://hdl.handle.net/10453/160806
dc.description.abstract	With the rapid development of quantum hardware, people tend to believe that special-purpose quantum computers with more than 100 qubits will be available in 5 to 10 years. It is conceivable that, once this becomes a reality, the development of quantum software will be crucial in harnessing the power of quantum computers. However, due to the distinguishable features of quantum mechanics, such as the no-cloning of quantum information and the nonlocal effect of entanglement, developing correct and efficient quantum programs and communication protocols is a challenging issue. Formal verification methods, particularly model checking techniques, have proven effective in classical software design and system modelling. Therefore, formal verification of quantum software has received more and more attention recently. This article reviews recent research findings in verification of both sequential quantum programs and quantum communication protocols, with the focus placed on the work of the two authors' research groups. Future directions and challenges in this area are also discussed.
dc.language	en
dc.relation.ispartof	Ruan Jian Xue Bao/Journal of Software
dc.relation.isbasedon	10.13328/j.cnki.jos.005536
dc.rights	info:eu-repo/semantics/closedAccess
dc.subject	0802 Computation Theory and Mathematics, 0803 Computer Software, 0805 Distributed Computing
dc.subject.classification	Software Engineering
dc.title	Verification of Quantum Programs
dc.type	Journal Article
utslib.citation.volume	29
utslib.for	0802 Computation Theory and Mathematics
utslib.for	0803 Computer Software
utslib.for	0805 Distributed Computing
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	*
dc.date.updated	2022-08-24T22:18:29Z
pubs.issue	4
pubs.publication-status	Published
pubs.volume	29
utslib.citation.issue	4

Abstract:

With the rapid development of quantum hardware, people tend to believe that special-purpose quantum computers with more than 100 qubits will be available in 5 to 10 years. It is conceivable that, once this becomes a reality, the development of quantum software will be crucial in harnessing the power of quantum computers. However, due to the distinguishable features of quantum mechanics, such as the no-cloning of quantum information and the nonlocal effect of entanglement, developing correct and efficient quantum programs and communication protocols is a challenging issue. Formal verification methods, particularly model checking techniques, have proven effective in classical software design and system modelling. Therefore, formal verification of quantum software has received more and more attention recently. This article reviews recent research findings in verification of both sequential quantum programs and quantum communication protocols, with the focus placed on the work of the two authors' research groups. Future directions and challenges in this area are also discussed.

Please use this identifier to cite or link to this item:

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