@inproceedings{gulwani2010the,
author = {Gulwani, Sumit and Zuleger, Florian},
title = {The Reachability-Bound Problem},
booktitle = {PLDI'10, June 5-10, 2010, Toronto, Ontario, Canada},
year = {2010},
month = {June},
abstract = {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.},
url = {http://approjects.co.za/?big=en-us/research/publication/reachability-bound-problem/},
edition = {PLDI’10, June 5–10, 2010, Toronto, Ontario, Canada},
}