  Quantum communication and cryptographic protocols are well on the way to
becoming an important practical technology. Although a large amount of
successful research has been done on proving their correctness, most of this
work does not make use of familiar techniques from formal methods, such as
formal logics for specification, formal modelling languages, separation of
levels of abstraction, and compositional analysis. We argue that these
techniques will be necessary for the analysis of large-scale systems that
combine quantum and classical components, and summarize the results of initial
investigation using behavioural equivalence in process calculus. This paper is
a summary of Simon Gay's invited talk at ICE'11.
