Compositional Recurrence Analysis Revisited
Zachary Kincaid, Jason Breck, Ashkan Forouhi Boroujeni, and Thomas Reps
Compositional recurrence analysis (CRA) is a static-analysis
method based on a 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 show how to address this impedance mismatch by augmenting the CRA
abstract domain with additional operations.
We call the resulting algorithm Interprocedural CRA (ICRA).
Our experiments with ICRA show that it has broad overall strength
compared with several state-of-the-art software model checkers.
The paper is an extended version, with proofs, of a paper
with the same title at PLDI 2017.
(Click here to access the paper:
PDF.)
University of Wisconsin