[Back]

S. Gulwani, F. Zuleger:
"The reachability-bound problem";
Talk: Conference on Programming Language Design and Implementation (PLDI), Toronto, Canada; 2010-06-05 - 2010-06-10; in: "PLDI'10 Proceedings of teh ACM SIGPLAN conference on Programming language design and implementation", B. G. Zorn, A. Aiken (ed.); PLDI'10 Proceedings of teh ACM SIGPLAN conference on Programming language design and implementation, (2010), ISBN: 978-1-4503-0019-3; 292 - 304.

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 information leakage or uncertainty propagation. Our approach to solving the reachability-bound problem brings together two 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 the 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.

http://dx.doi.org/10.1145/1806596.1806630