Techniques for Symbolic Complexity Bounds

Add to your list(s) Download to your calendar using vCal

• Eric Koskinen (University of Cambridge)
• Tuesday 18 November 2008, 13:00-14:00
• Computer Laboratory, William Gates Building, Room SS03.

If you have a question about this talk, please contact Thomas Tuerk.

Symbolic complexity bounds help programmers understand the performance characteristics of their implementations. Existing work provides techniques for statically determining bounds of procedures with only simple control-flow. However, procedures with nested loops or multiple paths through a single loop are challenging.

In this talk we describe two techniques that together enable estimation of precise bounds for procedures with nested and multi-path loops. The first technique transforms a multi-path loop into a semantically equivalent code fragment with simpler loops by making the structure of path-interleaving explicit. We show that his enables non-disjunctive invariant generation tools to find a bound on many procedures for which previous techniques were unable to prove termination. The second technique is to use invariants that characterize relationships between consecutive states that can arise at a program location. We further present an algorithm that uses these invariants to compute precise bounds for nested loops. The utility of each of the above techniques go beyond our application to symbolic bound analysis.

We have applied our methodology to a significant commercial product and were able to find symbolic bounds for 90% of the loops. We are not aware of any other published results that report experiences running a bound analysis on a real code-base.

This talk is part of the Computer Laboratory Automated Reasoning Group Lunches series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computer Laboratory Automated Reasoning Group Lunches
• Computer Laboratory, William Gates Building, Room SS03
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.