The “reachability-bound problem” is the problem of finding a symbolic worst-case bound on the number of times a given control location inside a procedure is visited in terms of the inputs to that procedure. This has applications in bounding resources consumed by a program such as time, memory, network-traffic, power, as well as estimating quantitative properties (as opposed to boolean properties) of data in programs, such as amount of information leakage or uncertainty propagation.

Our approach to solving the reachability-bound problem brings together three fundamentally different techniques for reasoning about loops in an effective manner. This includes (a) abstract-interpretation based iterative technique for computing precise disjunctive invariants to summarize nested loops, (b) arithmetic constraint solving based technique for computing ranking functions for individual paths inside loops, and (c) proof-rules based technique for appropriate composition of ranking functions for individual paths for precise loop bound computation.

We have implemented our solution to the reachability-bound problem in a tool called SPEED, which computes symbolic computational complexity bounds for procedures in .Net code-bases. The tool scales to large programs taking an average of around one second to analyze each procedure.