In quantum computing, the basic unit of information is a
qubit. Simulation of a general quantum program takes ex-
ponential time in the number of qubits, which makes simu-
lation infeasible beyond 50 qubits on current supercomput-
ers. So, for the understanding of larger programs, we turn to
static techniques. In this paper, we present an abstract inter-
pretation of quantum programs and we use it to automati-
cally verify assertions in polynomial time. Our key insight is
to let an abstract state be a tuple of projections. For such do-
mains, we present abstraction and concretization functions
that form a Galois connection and we use them to define ab-
stract operations. Our experiments on a laptop have verified
assertions about the Bernstein-Vazirani, GHZ, and Grover
benchmarks with 300 qubits.