We present a novel approach for the verification of control-centric safety properties in software based on a syntactic abstraction of data operations and the application of incremental induction on this abstraction. Unlike commonly-used abstractions, this abstraction is efficient to compute, preserves the structure of the program’s concrete transition relation, and is targeted for programs where computations on data are largely irrelevant to proving the given safety property (for example, in API usage verification). Specifically, data operations are treated as uninterpreted functions whereas control flow is captured using a novel one-hot encoding of the program counter. The abstraction is used in a standard CEGAR framework and either proves safety by generating an inductive invariant or produces an abstract counterexample that must be checked for concrete-level feasibility. Infeasibility can be due to the presence of spurious abstract states or transitions and is automatically eliminated with the addition of appropriate data lemmas that refine the abstract transition relation. A unique feature of the abstraction is that an abstract counterexample can be much shorter than its corresponding concrete counterpart. This verification approach has been implemented in the EUForia prototype tool which analyzes LLVM bitcode programs for assertion violations. The verification flow is completely automated, but is currently limited to C programs without dynamic allocation.