Abstract: Programming is error-prone. Programming a quantum computer and designing quantum communication protocols are even worse due to the weird nature of quantum systems. Therefore, verification techniques for quantum programs and quantum protocols will be indispensable whence commercial quantum computers and quantum communication systems are available. In the last 10 years, various verification techniques for classical programs including program logics and model-checking have been extended to deal with quantum programs. This talk summaries several results obtained by the author and his collaborators in this line of research.
