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.
|Institution||Technischen Universität Wien|