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, networktraffic, 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 abstractinterpretation 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 solver...

• Type: Conference
• Year: 2010
• Where: PLDI
• Authors: Sumit Gulwani, Florian Zuleger
• Keywords: Disjunctive Invariant Computation, PLDI 2010, Precise Disjunctive Invariants, Programming Languages, Symbolic Worst-case Bound