SPEED: precise and efficient static estimation of program computational complexity

This paper describes an inter-procedural technique for computing symbolic bounds on the number of statements a procedure executes in terms of its scalar inputs and user-defined quantitative functions of input data-structures. Such computational complexity bounds for even simple programs are usually disjunctive, non-linear, and involve numerical properties of heaps. We address the challenges of generating these bounds using two novel ideas. We introduce a proof methodology based on multiple counter instrumentation (each counter can be initialized and incremented at potentially multiple program locations) that allows a given linear invariant generation tool to compute linear bounds individually on these counter variables. The bounds on these counters are then composed together to generate total bounds that are non-linear and disjunctive. We also give an algorithm for automating this proof methodology. Our algorithm generates complexity bounds that are usually precise not only in terms o...

• Type: Conference
• Year: 2009
• Where: POPL
• Authors: Sumit Gulwani, Krishna K. Mehra, Trishul M. Chilimbi
• Keywords: Computational Complexity Bounds, Linear Bounds, POPL 2009, Programming Languages, Symbolic Complexity Bounds