Scaling Model Checking for Test Generation Using Dynamic Inference

Model checking engines employed to generate test cases covering the structure of the model or code are limited by factors like code size, loops and floating point computation. We propose an approach that overcomes these limitations by approximating code fragments by dynamically inferring their post-conditions. We use Daikon to infer likely invariants from execution traces, which are used as postconditions to compactly represent the state space computed by these code fragments. The resulting approximation enables application-level test case generation over larger code sizes using model checking, given the same resources of time, memory and computing power. Case studies show the efficacy of this approach.