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.