##
Path-Sensitive Resource Analysis Compliant with Assertions

Duc-Hiep Chu and Joxan Jaffar
#### Abstract

We consider the problem of bounding the worst-caseresourse usage of
loop-bounded programs, where assertions about valid program executions
may be enforced at selected program points. It is folklore that to be
precise, path-sensitivity is needed. This entails unrolling loops in
the manner of symbolic simulation. This in turn suggests that the
treatment of the individual loop iterations must be greedy in the
sense once analysis is finished on one iteration, we cannot backtrack
to change it. We show that under these conditions, enforcing
assertions produces unsound results.
We then present a two-phase algorithm with first uses a greedy strat-
egy in the unrolling of loops. This phase explores what is
conceptually a symbolic execution tree, which is of enormous size,
while eliminates infeasible paths and dominated paths that guaranteed
not to contribute to the worst case bound. A compact representation is
produced at the end of this phase. Finally, the second phase attacks
the remaining problem, to determine the worst-case path in the
simplified tree, excluding all paths that violate the assertions from
bound calculation. Scalability is achieved via an adaptation of a
dynamic programming algorithm.