Compositional recurrence analysis (CRA) is a static-analysis method based on an interesting combination of symbolic analysis and abstract interpretation. This paper addresses the problem of creating a context-sensitive interprocedural version of CRA that handles recursive procedures. The problem is non-trivial because there is an ``impedance mismatch'' between CRA, which relies on analysis techniques based on regular languages (i.e., Tarjan's path-expression method), and the context-free-language underpinnings of context-sensitive analysis.

We address this issue by showing that we can make use of a recently developed framework -- Newtonian Program Analysis via Tensor Product (NPA-TP) -- that reconciles this impedance mismatch when the abstract domain supports a few special operations. Our approach introduces new problems that are not addressed by NPA-TP; however, we are able to resolve those problems. We call the resulting algorithm Interprocedural CRA (ICRA).

Our experimental study of ICRA shows that it has broad overall strength. The study showed that ICRA is both faster and handles more assertions than two state-of-the-art software model checkers. It also performs well when applied to the problem of establishing bounds on resource usage, such as memory used or execution time.

(Click here to access the paper: PDF.)