Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs

Feng, Y; Li, S

Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs

Feng, Y

Li, S

Permalink

Publisher:: ACADEMIC PRESS INC ELSEVIER SCIENCE
Publication Type:: Journal Article
Citation:: Information and Computation, 2023, 294
Issue Date:: 2023-10-01

Embargoed

	Filename	Description	Size
	Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs.pdf	Accepted version	416.11 kB	Adobe PDF	View/Open

Copyright Clearance Process

Recently Added
In Progress
Embargoed
Open Access

This item is currently unavailable due to the publisher's embargo.

The embargo period expires on 1 Oct 2025

Full metadata record

Field	Value	Language
dc.contributor.author	Feng, Y https://orcid.org/0000-0002-3097-3896
dc.contributor.author	Li, S https://orcid.org/0000-0002-3332-2546
dc.date.accessioned	2024-02-06T01:36:30Z
dc.date.available	2024-02-06T01:36:30Z
dc.date.issued	2023-10-01
dc.identifier.citation	Information and Computation, 2023, 294
dc.identifier.issn	0890-5401
dc.identifier.issn	1090-2651
dc.identifier.uri	http://hdl.handle.net/10453/175344
dc.description.abstract	Abstract interpretation, Hoare logic, and incorrectness (or reverse Hoare) logic are powerful techniques for static analysis of computer programs. They have all been successfully extended to the quantum setting, but developed largely in parallel. This paper explores the relationship between these techniques in the context of verifying quantum while-programs, where the abstract domain and the set of assertions for quantum states are well-structured. We show that any complete quantum abstract interpretation induces a quantum Hoare logic and a quantum incorrectness logic, both being sound and relatively complete. Moreover, the induced logic systems operate in a forward manner, making them more suitable for certain applications. Conversely, any sound and relatively complete quantum Hoare logic or incorrectness logic induces a complete quantum abstract interpretation. As an application, we show the non-existence of any sound and relatively complete quantum Hoare logic or incorrectness logic if tuples of local subspaces are taken as assertions.
dc.language	English
dc.publisher	ACADEMIC PRESS INC ELSEVIER SCIENCE
dc.relation	http://purl.org/au-research/grants/arc/DP220102059
dc.relation.ispartof	Information and Computation
dc.relation.isbasedon	10.1016/j.ic.2023.105077
dc.rights	info:eu-repo/semantics/embargoedAccess
dc.subject	08 Information and Computing Sciences
dc.subject.classification	Computation Theory & Mathematics
dc.subject.classification	46 Information and computing sciences
dc.title	Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs
dc.type	Journal Article
utslib.citation.volume	294
utslib.for	08 Information and Computing Sciences
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	embargoed	*
utslib.copyright.embargo	2025-10-01T00:00:00+1000Z
dc.date.updated	2024-02-06T01:36:29Z
pubs.publication-status	Published
pubs.volume	294

Abstract:

Abstract interpretation, Hoare logic, and incorrectness (or reverse Hoare) logic are powerful techniques for static analysis of computer programs. They have all been successfully extended to the quantum setting, but developed largely in parallel. This paper explores the relationship between these techniques in the context of verifying quantum while-programs, where the abstract domain and the set of assertions for quantum states are well-structured. We show that any complete quantum abstract interpretation induces a quantum Hoare logic and a quantum incorrectness logic, both being sound and relatively complete. Moreover, the induced logic systems operate in a forward manner, making them more suitable for certain applications. Conversely, any sound and relatively complete quantum Hoare logic or incorrectness logic induces a complete quantum abstract interpretation. As an application, we show the non-existence of any sound and relatively complete quantum Hoare logic or incorrectness logic if tuples of local subspaces are taken as assertions.

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

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