Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Resource Bound Analysis of Imperative Programs

Florian Zuleger


For many practical applications it is important to bound the resources consumed by a program such as time, memory, network-traffic, power, and to estimate quantitative properties of data in programs, such as information leakage or uncertainty propagation. At the heart of many of these questions lies the problem of 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. 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. 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. We evaluate the effectiveness of this approach on a .Net base-class library and further benchmark programs. 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. We evaluate the effectiveness of this approach on two C benchmarks. We further present results towards a theoretical characterization of the bounds expressible by SCA. Finally we show that our solution to the reachability-bound problem captures the essential ideas of earlier termination and bound analyses and goes beyond in a simpler framework.


Publication typePhdThesis
InstitutionTechnischen Universität Wien
> Publications > Resource Bound Analysis of Imperative Programs