Date:
Thursday, May 05, 2011
Speaker:
Florian Zuleger
Venue: IST Austria
Notes:
Mondi 2
Computing bounds on the resource usage of a program often requires finding a symbolic worst-case bound on the number of visits to a given program location in terms of the inputs to that program; we call this the reachability-bound problem. The automatic computation of reachability-bounds is challenging because in general such bounds are complicated expressions that hinder the direct application of standard abstract domains and require disjunctive invariants.
We propose a two-step methodology for computing a reachability-bound of a given program location: First, we generate a transition system that disjunctively summarizes all pairs of states for which there is a program execution that visits the location once and again. Second, we compute a bound of the transition system to derive a reachability-bound. We present two approaches that implement this methodology.
Our first approach brings together an abstract-interpretation based iterative technique for computing disjunctive loop invariants and a non-iterative proof-rules based technique for loop bound computation.
Our second approach is based on the so-called size-change abstraction (SCA). We use a closure property of SCA for computing disjunctive loop invariants. We show that SCA offers a separation of concerns for bound computation: we extract local progress measures from small program parts, and then compose these local progress measures to a global bound. We state two program transformations that make imperative programs amenable to bound analysis with SCA.
