Constraints in one-to-many concretization for abstraction refinement

In one-to-many concretization for model checking based on abstraction refinement, constraints on input vectors that are pseudorandomly generated are often essential to the success of the procedure. These constraints have to do with both primary inputs and invisible state variables. We discuss algorithms that address both types and we show their effectiveness through experiments.