We define a small-step semantics for the untyped $\lambda$-calculus, that traces the $\beta$-reductions that occur during evaluation. By abstracting the computation traces, we reconstruct $k$-CFA using abstract interpretation, and justify constraint-based $k$-CFA in a semantic way. The abstract interpretation of the trace semantics also paves the way for introducing widening operators in CFA that go beyond existing analyses, that are all based on exploring a finite state space. We define $\nabla$CFA, a widening-based analysis that limits the cycles in call stacks, and can achieve better precision than $k$-CFA at a similar cost.