Talks and Poster Presentations (without Proceedings-Entry):
"Resource Bound Analysis of Imperative Programs";
Talk: RiSE Seminar,
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.
Created from the Publication Database of the Vienna University of Technology.