A Framework for Combining Analysis and Verification

We present a general framework for combining program verification and program analysis. This framework enhances program analysis because it takes advantage of user assertions, and it enhances program verification because assertions can be refined using automatic program analysis. Both enhancements in general produce a better way of reasoning about programs than using verification techniques alone or analysis techniques alone. More importantly, the combination is better than simply running the verification and analysis in isolation and then combining the results at the last step. In other words, our framework explores synergistic interaction between verification and analysis. In this paper, we start with a representation of a program, user assertions, and a given analyzer for the program. The framework we describe induces an algorithm which exploits the assertions and the analyzer to produce a generally more accurate analysis. Further, it has some important features: ffl it is flexible..