Compositional dynamic test generation

TLDR

Dynamic test generation, exemplified by DART, blends dynamic analysis with model checking to systematically execute all feasible program paths and detect errors via runtime checking. This paper tackles the scalability problem of exhaustive path execution by proposing compositional dynamic test generation that adapts interprocedural static analysis techniques. The SMART algorithm extends DART by testing functions in isolation, encoding results as precondition/postcondition summaries, and reusing those summaries to test higher‑level functions. Experiments show that SMART is sound and complete relative to DART, achieves identical path coverage, and reduces the number of executions from exponential to linear in the bound on feasible paths per function.

Abstract

Dynamic test generation is a form of dynamic program analysis that attempts to compute test inputs to drive a program along a specific program path. Directed Automated Random Testing, or DART for short, blends dynamic test generation with model checking techniques with the goal of systematically executing all feasible program paths of a program while detecting various types of errors using run-time checking tools (like Purify, for instance). Unfortunately, systematically executing all feasible program paths does not scale to large, realistic programs.This paper addresses this major limitation and proposes to perform dynamic test generation compositionally, by adapting known techniques for interprocedural static analysis. Specifically, we introduce a new algorithm, dubbed SMART for Systematic Modular Automated Random Testing, that extends DART by testing functions in isolation, encoding test results as function summaries expressed using input preconditions and output postconditions, and then re-using those summaries when testing higher-level functions. We show that, for a fixed reasoning capability, our compositional approach to dynamic test generation (SMART) is both sound and complete compared to monolithic dynamic test generation (DART). In other words, SMART can perform dynamic test generation compositionally without any reduction in program path coverage. We also show that, given a bound on the maximum number of feasible paths in individual program functions, the number of program executions explored by SMART is linear in that bound, while the number of program executions explored by DART can be exponential in that bound. We present examples of C programs and preliminary experimental results that illustrate and validate empirically these properties.