Digital filters are widely used in control/command programs: a digital filter is a numerical algorithm to smooth variations of sampled values of signal. Digital filters involve linear recursions that can hardly be bound by using linear invariants. We propose an abstract domain using quadratic constraints and formal expansion to bound the ranges of variables in digital filters.
