  Various techniques have been used in recent years for verifying quantum
computers, that is, for determining whether a quantum computer/system satisfies
a given formal specification of correctness. Barrier certificates are a recent
novel concept developed for verifying properties of dynamical systems. In this
article, we investigate the usage of barrier certificates as a means for
verifying behaviours of quantum systems. To do this, we extend the notion of
barrier certificates from real to complex variables. We then develop a
computational technique based on linear programming to automatically generate
polynomial barrier certificates with complex variables taking real values.
Finally, we apply our technique to several simple quantum systems to
demonstrate their usage.
