An automata-based framework for verification and bug hunting in quantum circuits

Yu-Fang Chen, Kai-Min Chung, Ond{\v r}ej Lengál, Jyun-Ao Lin, Wei-Lun Tsai, Di-De Yen
[doi] [Google Scholar] [DBLP] [Citeseer] [url]

Proc. ACM Program. Lang. 7(PLDI)
Association for Computing Machinery
New York, NY, USA
jun 2023
Note(s): verification, quantum computing

A bug-finding technique for quantum circuits that scales well and that avoids the more conventional floating point.

Idea is to model a vector of quantum bits as a weighted decision tree where the bits in the vector select the path through the tree. Quantum operators can be viewed as transformations on the tree (e.g., rotations, etc.)

Properties are written using Hoare-like notation “{P} c {Q}”