Verification of Java Programs with Interacting Analysis Plugins

In this paper we propose a modular framework for 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 show how to use our framework for static assertion checking by adapting the interprocedural dataflow analysis of Ball and Rajamani. We describe our implementation of a prototype checker for a subset of Java which combines predicate abstraction, 3-valued shape analysis and a decidable pointer analysis. We demonstrate through an example the increase in precision that our approach can provide.