A Symbolic Execution Method for Bounds Analysis
draft, (2009)http://www.comp.nus.edu.sg/~joxan/res.html.Abstract
Given a program whose loops are bounded, we address the problem of estimating the upper bound of a variable which is monotonically increasing, and its typical application in annotating a program so that bounds analysis produces an estimate of the worst-case resource usage. The method presented is a systematic enumeration of symbolic states of the program. The novelty is twofold: first, we use intermittent invariants, each being a property that is true of some but not all iterations of a loop. This allows for the discrimination of analyses of different iterations while still providing an abstraction so that the analysis can be practical. Second, we compute the bound estimate by simulating the behavior of the loop using a dynamic programming algorithm, relieving us from discovering a closed form expression for the loop. The analysis time of a loop, which reasons about all inputs, is then proportional to the actual running time of the loop, on one input. The method compared formally with prior work, and evaluated empirically on benchmark programs.