@fibso

Automatic Inference of Upper Bounds for Recurrence Relations in Cost Analysis

, , , and . Proceedings of the 15th International Symposium on Static Analysis, page 221--237. Berlin, Heidelberg, Springer-Verlag, (2008)
DOI: 10.1007/978-3-540-69166-2_15

Abstract

The classical approach to automatic cost analysis consists of two phases. Given a program and some measure of cost, we first produce <em>recurrence relations</em>(RRs) which capture the cost of our program in terms of the size of its input data. Second, we convert such RRs into <em>closed form</em>(i.e., without recurrences). Whereas the first phase has received considerable attention, with a number of cost analyses available for a variety of programming languages, the second phase has received comparatively little attention. In this paper we first study the features of RRs generated by automatic cost analysis and discuss why existing computer algebra systems are not appropriate for automatically obtaining closed form solutions nor upper bounds of them. Then we present, to our knowledge, the first practical framework for the fully automatic generation of reasonably accurate upper bounds of RRs originating from cost analysis of a wide range of programs. It is based on the inference of <em>ranking functions</em>and <em>loop invariants</em>and on <em>partial evaluation</em>.

Links and resources

Tags

community

  • @fibso
  • @dblp
@fibso's tags highlighted