We present a new method for the verification of quantum circuits based on a novel symbolic representation of sets of quantum states using level-synchronized tree automata (LSTAs). LSTAs extend classical tree automata by labeling each transition with a set of choices , which are then used to synchronize subtrees of an accepted tree. Compared to the traditional tree automata, LSTAs have an incomparable expressive power while maintaining important properties, such as closure under union and intersection, and decidable language emptiness and inclusion. We have developed an efficient and fully automated symbolic verification algorithm for quantum circuits based on LSTAs. The complexity of supported gate operations is at most quadratic, dramatically improving the exponential worst-case complexity of an earlier tree automata-based approach. Furthermore, we show that LSTAs are a promising model for parameterized verification , i.e., verifying the correctness of families of circuits with the same structure for any number of qubits involved, which principally lies beyond the capabilities of previous automated approaches.We implemented this method as a C++ tool and compared it with three symbolic quantum circuit verifiers and two simulators on several benchmark examples. The results show that our approach can solve problems with sizes orders of magnitude larger than the state of the art.

In this paper, genetic algorithms are proposed to shrink counterexamples found by QuickChick, a property-based testing framework for Coq. In order to make the outcome of property-based testing humanly understandable and inspectable, genetic algorithms are brought into the realm of rigorous software development as shrinkers capable of handling a broad range of data structures. In the present study, two showcases, merge sort and insertion of red-black trees, are investigated for illustrative purposes. Due to the lack of relevant results existing in the literature, two baseline methods, random sample and random walk are included in the experiments for comparison with the proposed genetic algorithm. The obtained results indicate that the proposal is effective since the program mistake can be identified with ease by examining the shrunk counterexamples and also that the adopted genetic algorithm statistically significantly outperforms random sample and random walk in both counterexample sizes and running time.