Invariants of quantum programs: Characterisations and generation

© 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