Abstract: We design specific domains for analyzing digital filtering. Digital filtering consists in implementing numerical recursions: the value of a variable S (the output) is computed from a fixed finite number of the last consecutive values of the variable S and from a fixed finite number of the last consecutive values of another variable E (the input). Our framework allows us to refine existing analyses so that they can handle given classes of digital filters. We only have to design a class of symbolic properties that describe the invariants throughout filter iterations, and to describe how these properties are transformed by filter iterations. Then, the analysis allows both inference and proofs of the properties about the program variables that are tied to any such filter. In case of linear filters, we propose a systematic method for designing the abstract domain by using intervals and ellipsoidal constraints.

@Misc{feret:NSAD05,
  author    = {J{\'e}r{\^o}me Feret},
  title     = {Numerical Abstract Domains for Digital Filters}
  booktitle = {International workshop on Numerical & Symbolic Abstract Domains (NSAD 2005)},
  year      = {2005},
}