  In this talk, we will describe a framework for assertion-based verification
(ABV) of quantum circuits by applying model checking techniques for quantum
systems developed in our previous work, in which:
  (i) Noiseless and noisy quantum circuits are modelled as operator- and
super-operator-valued transition systems, respectively, both of which can be
further represented by tensor networks.
  (ii) Quantum assertions are specified by a temporal extension of Birkhoff-von
Neumann quantum logic. Their semantics is defined based on the design decision:
they will be used in verification of quantum circuits by simulation on
classical computers or human reasoning rather than by quantum physics
experiments (e.g. testing through measurements);
  (iii) Algorithms for reachability analysis and model checking of quantum
circuits are developed based on contraction of tensor networks. We observe that
many optimisation techniques for computing relational products used in
BDD-based model checking algorithms can be generalised for contracting tensor
networks of quantum circuits.
