In this tutorial, the participants are introduced to Software Product Lines (SPLs) and in particular the field of behavioural variability modelling and analysis. They are made familiar with Featured Transition Systems (FTSs), Modal Transition Systems (MTSs) with variability constraints (MTSνs), and family-based analysis of such models. After explaining ambiguities in FTSs, the participants are introduced to SAT solving, and they are shown how to use it for static analysis of FTSs to detect ambiguities. Finally, a tool chain built around the Variability Model Checker VMC is presented, and it is demonstrated how to use VMC to perform an efficient kind of family-based model checking of deadlock-free FTSs and MTSs. It is also demonstrated how to use the front-end tool FTS4VMC to detect and remove ambiguities in an FTS, and to transform the resulting FTS into an MTS to make it amenable for analysis with VMC.