Most Influential Paper Award

Presented for
Model Checking Lots of Systems: Efficient Verification of Temporal Properties in Software Product Lines
32nd International Conference on Software Engineering (ICSE 2010)

This paper was the first to consider features at first-class citizens in modeling SPL behavior, resulting in the first rigorous account of behavioral variability and an associated rigorous family-based verification method.
This paper introduced the notion of a Featured Transition System (FTS) to the community, allowing scalable SPL modeling. Concretely, the authors extended labeled transition systems with features in order to concisely describe and analyze the combined behavior of a family of behavioral models. The paper also introduced dedicated family-based model-checking techniques that have enriched model-checking algorithms by offering a means to verify whether a property is satisfied by an FTS, in which case it is also satisfied by every product of the SPL, and if a property is violated, then the algorithm reports a counterexample as well as the products of the SPL that violate the property.
Overall, by carving out the right concept, this paper paved the way for a vast amount of research on formal analysis (testing, model checking, etc.) of variability in behavioral models of SPLs and configurable systems in general, and contributed to their dissemination in industrial settings. A number of SPL analysis tools nowadays accept FTSs as input format. In fact, FTSs have become the de-facto standard formalism for the formal analysis of behavior of models with variability.