Quantum abstract interpretation

Yu, N; Palsberg, J

Quantum abstract interpretation

Yu, N

Palsberg, J

Permalink

Publisher:: ASSOC COMPUTING MACHINERY
Publication Type:: Conference Proceeding
Citation:: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2021, pp. 542-558
Issue Date:: 2021-06-18

Closed Access

	Filename	Description	Size
	pldi21-quantum.pdf	Published version	304.22 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	Yu, N https://orcid.org/0000-0003-1188-3032
dc.contributor.author	Palsberg, J
dc.contributor.editor	Freund, SN
dc.contributor.editor	Yahav, E
dc.date	2021-06-20
dc.date.accessioned	2022-03-31T03:57:27Z
dc.date.available	2022-03-31T03:57:27Z
dc.date.issued	2021-06-18
dc.identifier.citation	Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2021, pp. 542-558
dc.identifier.isbn	9781450383912
dc.identifier.uri	http://hdl.handle.net/10453/155764
dc.description.abstract	In quantum computing, the basic unit of information is a qubit. Simulation of a general quantum program takes exponential time in the number of qubits, which makes simulation infeasible beyond 50 qubits on current supercomputers. So, for the understanding of larger programs, we turn to static techniques. In this paper, we present an abstract interpretation of quantum programs and we use it to automatically verify assertions in polynomial time. Our key insight is to let an abstract state be a tuple of projections. For such domains, we present abstraction and concretization functions that form a Galois connection and we use them to define abstract operations. Our experiments on a laptop have verified assertions about the Bernstein-Vazirani, GHZ, and Grover benchmarks with 300 qubits.
dc.language	en
dc.publisher	ASSOC COMPUTING MACHINERY
dc.relation.ispartof	Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)
dc.relation.ispartof	42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI)
dc.relation.isbasedon	10.1145/3453483.3454061
dc.rights	info:eu-repo/semantics/closedAccess
dc.title	Quantum abstract interpretation
dc.type	Conference Proceeding
utslib.location.activity	ELECTR NETWORK
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-03-31T03:57:26Z
pubs.finish-date	2021-06-25
pubs.publication-status	Published
pubs.start-date	2021-06-20

Abstract:

In quantum computing, the basic unit of information is a qubit. Simulation of a general quantum program takes exponential time in the number of qubits, which makes simulation infeasible beyond 50 qubits on current supercomputers. So, for the understanding of larger programs, we turn to static techniques. In this paper, we present an abstract interpretation of quantum programs and we use it to automatically verify assertions in polynomial time. Our key insight is to let an abstract state be a tuple of projections. For such domains, we present abstraction and concretization functions that form a Galois connection and we use them to define abstract operations. Our experiments on a laptop have verified assertions about the Bernstein-Vazirani, GHZ, and Grover benchmarks with 300 qubits.

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

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