Software product line analysis with mCRL2
M.A. ter Beek and E.P. de Vink

The mCRL2 language and supporting software provide a state-of-the-art
toolset for the verification of distributed systems, which can also be
used for variability analysis of software product lines from a
behavioural perspective. Moreover, by their feature-oriented nature,
software product lines and accompanying behavior models lend
themselves to a refactoring into a parallel composition of components
reflecting coherent sets of features. This opens the way for dedicated
abstraction and reduction techniques that strengthen the prospect of a
scalable verification approach to software product lines.