Sciweavers

Share
POPL
2009
ACM

SPEED: precise and efficient static estimation of program computational complexity

12 years 2 months ago
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...
Sumit Gulwani, Krishna K. Mehra, Trishul M. Chilim
Added 22 Nov 2009
Updated 22 Nov 2009
Type Conference
Year 2009
Where POPL
Authors Sumit Gulwani, Krishna K. Mehra, Trishul M. Chilimbi
Comments (0)
books