Framework for combining analysis and verification

Abstract

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: it is flexible: any number of assertions can be used anywhere; it is open: it can employ an arbitrary analyzer; it is modular: we reason with conditional correctness of assertions; it is incremental: it can be tuned for the accuracy/efficiency tradeoff.