  In this work, we show how the use of verification and analysis techniques for
model families (software product lines) with numerical features provides an
interesting technique to synthesize complete models from sketches (i.e.\
partial models with holes). In particular, we present an approach for
synthesizing Promela model sketches using variability-specific abstraction
refinement for lifted (family-based) model checking.
