The Reachability-Bound Problem
We define the reachability-bound problem to be 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
two very different techniques for reasoning about loops in an
effective manner. One of these techniques is an
abstract-interpretation based iterative technique for computing
precise disjunctive invariants (to summarize nested loops).
The other technique is a
non-iterative proof-rules based technique (for loop bound
computation) that takes over the role of doing inductive reasoning,
while deriving its power from use of SMT solvers to reason about
abstract loop-free fragments.
Our solution to the reachability-bound problem allows us to compute
precise symbolic complexity bounds for several loops in .Net base-class
libraries for which earlier techniques fail. We also illustrate the
precision of our algorithm for disjunctive invariant computation (which
has a more general applicability beyond the reachability-bound problem)
on a set of benchmark examples.