On incorrectness logic for Quantum programs

Yan, P; Jiang, H; Yu, N

On incorrectness logic for Quantum programs

Yan, P Jiang, H Yu, N

Permalink

Publisher:: Association for Computing Machinery (ACM)
Publication Type:: Journal Article
Citation:: Proceedings of the ACM on Programming Languages, 2022, 6, (OOPSLA1), pp. 1-28
Issue Date:: 2022-04-29

Open Access

Copyright Clearance Process

Recently Added
In Progress
Open Access

This item is open access.

Adobe PDF

Download full textAdobe PDF (362.38 kB)

View on publisher's site

View statistics

Full metadata record

Field	Value	Language
dc.contributor.author	Yan, P
dc.contributor.author	Jiang, H
dc.contributor.author	Yu, N https://orcid.org/0000-0003-1188-3032
dc.date.accessioned	2023-03-21T00:46:24Z
dc.date.available	2023-03-21T00:46:24Z
dc.date.issued	2022-04-29
dc.identifier.citation	Proceedings of the ACM on Programming Languages, 2022, 6, (OOPSLA1), pp. 1-28
dc.identifier.issn	2475-1421
dc.identifier.issn	2475-1421
dc.identifier.uri	http://hdl.handle.net/10453/167858
dc.description.abstract	Bug-catching is important for developing quantum programs. Motivated by the incorrectness logic for classical programs, we propose an incorrectness logic towards a logical foundation for static bug-catching in quantum programming. The validity of formulas in this logic is dual to that of quantum Hoare logics. We justify the formulation of validity by an intuitive explanation from a reachability point of view and a comparison against several alternative formulations. Compared with existing works focusing on dynamic analysis, our logic provides sound and complete arguments. We further demonstrate the usefulness of the logic by reasoning several examples, including Grover's search, quantum teleportation, and a repeat-until-success program. We also automate the reasoning procedure by a prototyped static analyzer built on top of the logic rules.
dc.language	en
dc.publisher	Association for Computing Machinery (ACM)
dc.relation.ispartof	Proceedings of the ACM on Programming Languages
dc.relation.isbasedon	10.1145/3527316
dc.rights	info:eu-repo/semantics/openAccess
dc.title	On incorrectness logic for Quantum programs
dc.type	Journal Article
utslib.citation.volume	6
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	open_access	*
dc.date.updated	2023-03-21T00:46:23Z
pubs.issue	OOPSLA1
pubs.publication-status	Published
pubs.volume	6
utslib.citation.issue	OOPSLA1

Abstract:

Bug-catching is important for developing quantum programs. Motivated by the incorrectness logic for classical programs, we propose an incorrectness logic towards a logical foundation for static bug-catching in quantum programming. The validity of formulas in this logic is dual to that of quantum Hoare logics. We justify the formulation of validity by an intuitive explanation from a reachability point of view and a comparison against several alternative formulations. Compared with existing works focusing on dynamic analysis, our logic provides sound and complete arguments. We further demonstrate the usefulness of the logic by reasoning several examples, including Grover's search, quantum teleportation, and a repeat-until-success program. We also automate the reasoning procedure by a prototyped static analyzer built on top of the logic rules.

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

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