Formal verification of quantum algorithms using quantum hoare logic

Liu, J; Zhan, B; Wang, S; Ying, S; Liu, T; Li, Y; Ying, M; Zhan, N

Formal verification of quantum algorithms using quantum hoare logic

Liu, J Zhan, B Wang, S Ying, S Liu, T Li, Y Ying, M

Zhan, N

Permalink

Publisher:: SPRINGER INTERNATIONAL PUBLISHING AG
Publication Type:: Conference Proceeding
Citation:: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2019, 11562 LNCS, pp. 187-207
Issue Date:: 2019-01-01

Closed Access

	Filename	Description	Size
	Liu2019_Chapter_FormalVerificationOfQuantumAlg.pdf		357.03 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	Liu, J
dc.contributor.author	Zhan, B
dc.contributor.author	Wang, S
dc.contributor.author	Ying, S
dc.contributor.author	Liu, T
dc.contributor.author	Li, Y
dc.contributor.author	Ying, M https://orcid.org/0000-0003-4847-702X
dc.contributor.author	Zhan, N
dc.contributor.editor	Dillig, I
dc.contributor.editor	Tasiran, S
dc.date	2019-07-15
dc.date.accessioned	2020-05-11T06:58:44Z
dc.date.available	2020-05-11T06:58:44Z
dc.date.issued	2019-01-01
dc.identifier.citation	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2019, 11562 LNCS, pp. 187-207
dc.identifier.isbn	9783030255428
dc.identifier.issn	0302-9743
dc.identifier.issn	1611-3349
dc.identifier.uri	http://hdl.handle.net/10453/140634
dc.description.abstract	© The Author(s) 2019. We formalize the theory of quantum Hoare logic (QHL) [TOPLAS 33(6),19], an extension of Hoare logic for reasoning about quantum programs. In particular, we formalize the syntax and semantics of quantum programs in Isabelle/HOL, write down the rules of quantum Hoare logic, and verify the soundness and completeness of the deduction system for partial correctness of quantum programs. As preliminary work, we formalize some necessary mathematical background in linear algebra, and define tensor products of vectors and matrices on quantum variables. As an application, we verify the correctness of Grover’s search algorithm. To our best knowledge, this is the first time a Hoare logic for quantum programs is formalized in an interactive theorem prover, and used to verify the correctness of a nontrivial quantum algorithm.
dc.language	en
dc.publisher	SPRINGER INTERNATIONAL PUBLISHING AG
dc.relation.ispartof	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
dc.relation.ispartof	31st International Conference on Computer-Aided Verification (CAV)
dc.relation.isbasedon	10.1007/978-3-030-25543-5_12
dc.rights	info:eu-repo/semantics/restrictedAccess
dc.subject.classification	Artificial Intelligence & Image Processing
dc.title	Formal verification of quantum algorithms using quantum hoare logic
dc.type	Conference Proceeding
utslib.citation.volume	11562 LNCS
utslib.location.activity	New York, NY
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
pubs.organisational-group	/University of Technology Sydney
utslib.copyright.status	closed_access	*
dc.date.updated	2020-05-11T06:58:42Z
pubs.finish-date	2019-07-18
pubs.publication-status	Published
pubs.start-date	2019-07-15
pubs.volume	11562 LNCS
utslib.start-page	187

Abstract:

© The Author(s) 2019. We formalize the theory of quantum Hoare logic (QHL) [TOPLAS 33(6),19], an extension of Hoare logic for reasoning about quantum programs. In particular, we formalize the syntax and semantics of quantum programs in Isabelle/HOL, write down the rules of quantum Hoare logic, and verify the soundness and completeness of the deduction system for partial correctness of quantum programs. As preliminary work, we formalize some necessary mathematical background in linear algebra, and define tensor products of vectors and matrices on quantum variables. As an application, we verify the correctness of Grover’s search algorithm. To our best knowledge, this is the first time a Hoare logic for quantum programs is formalized in an interactive theorem prover, and used to verify the correctness of a nontrivial quantum algorithm.

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

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