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}”