[Back]

F. Zuleger:
"Resource Bound Analysis of Imperative Programs";
Talk: RiSE Seminar, Klosterneuburg; 2011-05-05.

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.