POPL 2017
Sun 15 - Sat 21 January 2017
Fri 20 Jan 2017 16:30 - 16:55 at Amphitheater 44 - Quantum Chair(s): Michele Pagani

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 verification and analysis of quantum programs. Interestingly, the notion of invariant can be defined for quantum programs in two different ways – additive invariants and multiplicative invariants – corresponding to two interpretations of implication in a continuous valued logic: the Lukasiewicz implication and the Godel implication. It is shown that both of them can be used to establish partial correctness of quantum programs. The problem of generating additive 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 sampling. Our examples show that the generated invariants can be used to verify correctness of these algorithms and are helpful in optimising 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.

Fri 20 Jan

POPL-2017-papers
16:30 - 17:45: POPL - Quantum at Amphitheater 44
Chair(s): Michele PaganiIRIF, Université Paris Diderot
POPL-2017-papers16:30 - 16:55
Talk
Mingsheng YingUniversity of Technology Sydney, Australia, Shenggang YingUniversity of Technology Sydney, Australia, Xiaodi WuUniversity of Oregon, USA
POPL-2017-papers16:55 - 17:20
Talk
Ugo Dal LagoUniversity of Bologna, France, Claudia Faggian, Benoit ValironLRI, CentraleSupelec, Univ. Paris Saclay, Akira YoshimizuUniv.Tokyo
POPL-2017-papers17:20 - 17:45
Talk
Jennifer Paykin, Robert RandUniversity of Pennsylvania, Steve ZdancewicUniversity of Pennsylvania