Control-flow refinement and progress invariants for bound analysis
Sumit Gulwani, Sagar C. Jain, Eric Koskinen · 2009
Symbolic complexity bounds help programmers understand the performance characteristics of their implementations. Existing work provides techniques for statically determining bounds of procedures with simple control-flow. However, procedures with nested loops or multiple paths through a single loop are challenging.