We propose efficient family-based Software Product Lines (SPL) model checking  based on variability parity games. These extend parity games with conditional edges labelled with (feature) configurations. We validate our contribution by experiments on SPL benchmark models, which demonstrate that a novel family-based algorithm to collectively solve variability parity games, using symbolic representations of the configuration sets, outperforms in all cases the product-based method of solving standard parity games obtained by projection with classical algorithms.

Joint work with Maurice ter Beek, Sjef van Loo and Erik de Vink