Flemming Nielson, Hanne Riis Nielson and Helmut Seidl. Automatic Complexity Analysis. In Daniel Le Métayer, editor, Programming Languages and Systems, volume 2305 of Lecture Notes in Computer Science, pages 243-261, Grenoble, France, April 2002. Springer.

We consider the problem of automating the derivation of tight asymptotic complexity bounds for solving Horn clauses. Clearly, the solving time crucially depends on the “sparseness” of the computed relations. Therefore, our asymptotic runtime analysis is accompanied by an asymptotic sparsity calculus together with an asymptotic sparsity analysis. The technical problem here is that least fixpoint iteration fails on asymptotic complexity expressions: the intuitive reason is that (1)+ (1) = (1) but (1) + ⋯ + (1) may return any value.

Download: PDF Reference: Bibtex The original publication is available at www.springerlink.com