Model Checking Quantum Systems --- A Survey <s> 3) Analysis and verification of quantum programs: <s> Floyd--Hoare logic is a foundation of axiomatic semantics of classical programs, and it provides effective proof techniques for reasoning about correctness of classical programs. To offer similar techniques for quantum program verification and to build a logical foundation of programming methodology for quantum computers, we develop a full-fledged Floyd--Hoare logic for both partial and total correctness of quantum programs. It is proved that this logic is (relatively) complete by exploiting the power of weakest preconditions and weakest liberal preconditions for quantum programs. <s> BIB001 </s> Model Checking Quantum Systems --- A Survey <s> 3) Analysis and verification of quantum programs: <s> Abstract We present ScaffCC, a scalable compilation and analysis framework based on LLVM (Lattner and Adve, 2004), which can be used for compiling quantum computing applications at the logical level. Drawing upon mature compiler technologies, we discuss similarities and differences between compilation of classical and quantum programs, and adapt our methods to optimizing the compilation time and output for the quantum case. Our work also integrates a reversible-logic synthesis tool in the compiler to facilitate coding of quantum circuits. Lastly, we present some useful quantum program analysis scenarios and discuss their implications, specifically with an elaborate discussion of timing analysis for critical path estimation. Our work focuses on bridging the gap between high-level quantum algorithm specifications and low-level physical implementations, while providing good scalability to larger and more interesting problems. <s> BIB002 </s> Model Checking Quantum Systems --- A Survey <s> 3) Analysis and verification of quantum programs: <s> Foundations of Quantum Programming discusses how new programming methodologies and technologies developed for current computers can be extended to exploit the unique power of quantum computers, which promise dramatic advantages in processing speed over currently available computer systems. Governments and industries around the globe are now investing vast amounts of money with the expectation of building practical quantum computers. Drawing upon years of experience and research in quantum computing research and using numerous examples and illustrations, Mingsheng Ying has created a very useful reference on quantum programming languages and important tools and techniques required for quantum programming, making the book a valuable resource for academics, researchers, and developers. Demystifies the theory of quantum programming using a step-by-step approach Covers the interdisciplinary nature of quantum programming by providing examples from many different fields including, engineering, computer science, medicine, and life sciences Includes techniques and tools to solve complex control flow patterns and synchronize computations Presents a coherent and self-contained treatment that will be valuable for academics and industrial researchers and developers <s> BIB003 </s> Model Checking Quantum Systems --- A Survey <s> 3) Analysis and verification of quantum programs: <s> 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. <s> BIB004 </s> Model Checking Quantum Systems --- A Survey <s> 3) Analysis and verification of quantum programs: <s> We introduce the notion of linear ranking super-martingale (LRSM) for quantum programs (with nondeterministic choices, namely angelic and demonic choices). Several termination theorems are established showing that the existence of the LRSMs of a quantum program implies its termination. Thus, the termination problems of quantum programs is reduced to realisability and synthesis of LRSMs. We further show that the realisability and synthesis problem of LRSMs for quantum programs can be reduced to an SDP (Semi-Definite Programming) problem, which can be settled with the existing SDP solvers. The techniques developed in this paper are used to analyse the termination of several example quantum programs, including quantum random walks and quantum Bernoulli factory for random number generation. This work is essentially a generalisation of constraint-based approach to the corresponding problems for probabilistic programs developed in the recent literature by adding two novel ideas: (1) employing the fundamental Gleason’s theorem in quantum mechanics to guide the choices of templates; and (2) a generalised Farkas’ lemma in terms of observables (Hermitian operators) in quantum physics. <s> BIB005
Another important application area of classical model-checking is analysis and verification of programs. Several techniques for analysis and verification of quantum programs have been reported in the last few years BIB002 , BIB001 , BIB003 , BIB004 , BIB005 . However, model-checking techniques specifically designed for quantum programs are still missing. 4) Verification of security of quantum communication protocols: Applications of model-checking mentioned in Section II focus on verification of correctness of quantum communication protocols. But verification of the security of quantum protocols is much more difficult, and model-checking applied to it is an interesting topic for future research. Finally, a crucial step toward real-world applications of modelchecking would be building efficient automatic tools.