In this paper we propose and argue for a modular framework for interprocedural program analysis,
where multiple program analysis tools are combined in order to exploit the particular advantages of
each. This allows for “plugging together” such tools as required by each verification task and makes it easy
to integrate new analyses. Our framework automates the sharing of information between plugins using a first
order logic with transitive closure, in a way inspired by the open product of Cortesi et al..
We describe a prototype implementation of our framework, which performs static assertion checking on
a simple language for heap-manipulating programs. This implementation includes plugins for three existing
approaches — predicate abstraction, 3-valued shape analysis and a decidable pointer analysis — and for a
simple type system. We demonstrate through a detailed example the increase in precision that our approach
can provide. Finally we discuss the design decisions we have taken, in particular the tradeoffs involved in
the choice of language by which the plugins communicate, and identify some future directions for our work.