|Year of Publication||2003|
|Authors||Bagnara R, Zaccagnini A, Zolo T|
|Keywords||complexity analysis, recurrence relations, software verification, static analysis|
We describe algorithmic techniques for the efficient solution of a wide class of linear recurrences of finite order with constant coefficients. We give an outline of the underlying theory both from an abstract and a more concrete point of view, in an attempt to convey the general principles as clearly as possible yet providing a well marked path for the implementation. In particular, the presentation is thorough and reasonably self-contained, covering topics such as the automatic solution of polynomial equations and efficient, exact symbolic summation of some special functions.