Verification of quantum circuits

We are at the dawn of a new "computing age" in which quantum computers will find their way into practical applications. Although quantum computers work differently than classical machines, the design flow for realizing applications is similar: first, the desired functionality/application is described on a high level. Then, it is compiled down to a description (usually called quantum circuit) that can be executed on an actual machine. During this process, lots of constraints have to be fulfilled, and optimizations are applied to reduce the circuit's size and, hence, improve the actual performance on the quantum computer - all of which are highly nontrivial steps. As in conventional design, sooner or later, it is essential to check whether the resulting realization is correct - motivating verification. This chapter reviews and provides a summary of work in this regard. Considering the challenges currently seen in the verification of (comparatively simpler) classical systems, this may provide the basis for preventing the emergence of a verification gap in quantum computing.