We explain the basic concepts of Event-B, that is the specification of machines and refinement, in light of abstract interpretation. After formally defining the trace semantics of systems handled by Event-B, we show that machines are specifications of abstractions of this semantics while refinement is an inverse abstract interpretation reducing the degree of nondeterminism of this trace semantics. We conclude by proposing in induction principle for program verification exploiting both property abstraction and program refinement.