Improved Visibility in One-to-Many Trace Concretization

We present an improved algorithm for concretization of abstract error traces in abstraction refinement-based invariant checking. The proposed algorithm maps each transition of the abstract error trace to one or more transitions in the concrete model by using a combination of simulation and satisfiability checking. Prior simulation- based approaches were hindered by limited visibility, which often resulted in excessive backtracking or refinements. The proposed technique addresses this issue in three ways: By identifying variables whose addition to the abstract trace significantly improves its predictive power at a low computational cost; by combining SAT checks with pseudo-random simulation in the construction of the concrete trace; and by a more flexible budgeting of simulation vectors that accounts for the progress made in concretization.