Invariants of quantum programs: Characterisations and generation

Ying, M; Ying, S; Wu, X

Invariants of quantum programs: Characterisations and generation

Ying, M

Ying, S Wu, X

Permalink

Publication Type:: Conference Proceeding
Citation:: Conference Record of the Annual ACM Symposium on Principles of Programming Languages, 2017, pp. 818 - 832
Issue Date:: 2017-01-01

Open Access

Copyright Clearance Process

Recently Added
In Progress
Open Access

This item is open access.

Adobe PDF

Download Accepted ManuscriptAdobe PDF (1.23 MB)

View on publisher's site

View statistics

Full metadata record

Field	Value	Language
dc.contributor.author	Ying, M https://orcid.org/0000-0003-4847-702X	en_US
dc.contributor.author	Ying, S	en_US
dc.contributor.author	Wu, X	en_US
dc.date.issued	2017-01-01	en_US
dc.identifier.citation	Conference Record of the Annual ACM Symposium on Principles of Programming Languages, 2017, pp. 818 - 832	en_US
dc.identifier.isbn	9781450346603	en_US
dc.identifier.issn	0730-8566	en_US
dc.identifier.uri	http://hdl.handle.net/10453/127333
dc.description.abstract	© 2017 ACM. Program invariant is a fundamental notion widely used in program verification and analysis. The aim of this paper is twofold: (i) find an appropriate definition of invariants for quantum programs; and (ii) develop an effective technique of invariant generation for ver- ification and analysis of quantum programs. Interestingly, the no- tion of invariant can be defined for quantum programs in two d- ifferent ways - additive invariants and multiplicative invariants - corresponding to two interpretations of implication in a continuous valued logic: the £ukasiewicz implication and the Godel implica- tion. It is shown that both of them can be used to establish partial correctness of quantum programs. The problem of generating ad- ditive invariants of quantum programs is addressed by reducing it to an SDP (Semidefinite Programming) problem. This approach is applied with an SDP solver to generate invariants of two important quantum algorithms - quantum walk and quantum Metropolis sam- pling. Our examples show that the generated invariants can be used to verify correctness of these algorithms and are helpful in optimis- ing quantum Metropolis sampling. To our knowledge, this paper is the first attempt to define the notion of invariant and to develop a method of invariant generation for quantum programs.	en_US
dc.relation.ispartof	Conference Record of the Annual ACM Symposium on Principles of Programming Languages	en_US
dc.relation.isbasedon	10.1145/3009837.3009840	en_US
dc.title	Invariants of quantum programs: Characterisations and generation	en_US
dc.type	Conference Proceeding
utslib.for	0802 Computation Theory and Mathematics	en_US
pubs.embargo.period	Not known	en_US
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
pubs.publication-status	Published	en_US

Abstract:

© 2017 ACM. Program invariant is a fundamental notion widely used in program verification and analysis. The aim of this paper is twofold: (i) find an appropriate definition of invariants for quantum programs; and (ii) develop an effective technique of invariant generation for ver- ification and analysis of quantum programs. Interestingly, the no- tion of invariant can be defined for quantum programs in two d- ifferent ways - additive invariants and multiplicative invariants - corresponding to two interpretations of implication in a continuous valued logic: the £ukasiewicz implication and the Godel implica- tion. It is shown that both of them can be used to establish partial correctness of quantum programs. The problem of generating ad- ditive invariants of quantum programs is addressed by reducing it to an SDP (Semidefinite Programming) problem. This approach is applied with an SDP solver to generate invariants of two important quantum algorithms - quantum walk and quantum Metropolis sam- pling. Our examples show that the generated invariants can be used to verify correctness of these algorithms and are helpful in optimis- ing quantum Metropolis sampling. To our knowledge, this paper is the first attempt to define the notion of invariant and to develop a method of invariant generation for quantum programs.

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

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