Statically Validating Must Summaries for Incremental Compositional Dynamic Test Generation

Compositional dynamic test generation can achieve significant scalability by memoizing symbolic execution sub-paths as test summaries. In this paper, we formulate the problem of statically validating symbolic test summaries against code changes. Summaries that can be proved still valid using a static analysis of a new program version do not need to be retested or recomputed dynamically. In the presence of small code changes, incrementality can considerably speed up regression testing since static checking is much cheaper than dynamic checking and testing. We provide several checks ranging from simple syntactic ones to ones that use a theorem prover. We present preliminary experimental results comparing these approaches on three large Windows applications.