BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Techniques for Symbolic Complexity Bounds - Eric Koskinen (Univers
 ity of Cambridge)
DTSTART:20081118T130000Z
DTEND:20081118T140000Z
UID:TALK13425@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:Symbolic complexity bounds help programmers understand the per
 formance characteristics of their implementations. Existing work provides 
 techniques for statically determining bounds of procedures with only simpl
 e control-flow. However\, procedures with nested loops or multiple paths 
 through a single loop are challenging.\n\nIn this talk we describe two tec
 hniques that together enable estimation of precise bounds for procedures w
 ith nested and multi-path loops. The first technique transforms a multi-pa
 th loop into a semantically equivalent code fragment with simpler loops by
  making the structure of path-interleaving explicit. We show that his enab
 les non-disjunctive invariant generation tools to find a bound on many pr
 ocedures for which previous techniques were unable to prove termination. T
 he second technique is to use invariants that characterize relationships b
 etween 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 o
 ur application to symbolic bound analysis.\n\nWe have applied our methodol
 ogy to a significant commercial product and were able to find symbolic b
 ounds for 90% of the loops. We are not aware of any other published result
 s that report experiences running a  \nbound analysis on a real code-base.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR