Compositional dynamic test generation can achieve significant scat-ability 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 anal-ysis of a new program version do not need to be retested or recomputed dynam-ically. 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 re-sults comparing these approaches on three large Windows applications.
展开▼
