Information Exchange Between Over- and Underapproximating Software Analyses

Abstract

Cooperative software validation aims at having verification and/or testing tools cooperate on the task of correctness checking. Cooperation involves the exchange of information about currently achieved results in the form of (verification) artifacts. These artifacts are typically specialized to the type of analysis performed by the tool, e.g. bounded model checking, abstract interpretation or symbolic execution, and hence requires the definition of a new artifact for every new cooperation to be built. In this paper, we introduce a unified artifact (called Generalized Information Exchange Automaton, short GIA) supporting the cooperation of overapproximating with underapproximating analyses. It provides all the information gathered by an analysis to its partner in a cooperation, independent of the type of analysis and usage context. We provide a formal definition of this artifact as an automaton together with two operators on GIAs, the first reducing a program with respect to results in a GIA and the second combining partial results in two GIAs into one. We show that computed analysis results are never lost when connecting tools via reducers and combiners. To experimentally demonstrate the feasibility, we have implemented one such cooperation and report on the achieved results, in particular how the new artifact is able to overcome some of the drawbacks of existing artifacts.