(Semantic) Feature Model Differences with (Q)SAT

Feature models evolve in multiple iterations over time. When modellers change a model, they enact syntactical changes in order to produce specific semantic differences between model iterations. Many tools have been developed to analyze such syntactical differences, but the changing semantics of models were harder to assess. Tools for semantic differences between feature model iterations rely on Binary Decision Diagrams (BDDs) or encode each change into SAT, the former leading to BDD scaling issues and the latter requiring editor support or other specialized tooling. We contribute the first concise formalization of feature models and their semantic differences into propositional logic and use it to efficiently and scalably classify semantic differences using SAT solvers. We then extend our definition into QSAT in order to quantify the full list of semantic differences between feature models and enumerate them using QBF tools, without needing specialized feature model solvers. We implement a semantic difference classifier using our UVL processing pipeline based on Booleguru (instead of the more widely used FeatureIDE) and evaluate it on industrial feature model instances in the standardized UVL format. We also evaluate our QSAT-based semantic difference enumerator and reproduce prior results. We provide all software and evaluation results in an artifact.
Fri 13 JunDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
13:30 - 15:00 | |||
13:30 22mTalk | Optimize Effect Handling for Tail-resumption with Stack Unwinding SLE 2025 | ||
13:52 22mTalk | Variability Fault Localization by Abstract Interpretation and its Application to SPL Repair SLE 2025 Aleksandar S. Dimovski Mother Teresa University, Skopje | ||
14:15 22mTalk | (Semantic) Feature Model Differences with (Q)SAT SLE 2025 Simone Heisinger JKU Linz, Maximilian Heisinger JKU Linz, Martina Seidl Johannes Kepler University Linz | ||
14:37 22mTalk | Detecting Resource Leaks on Android with Alpakka SLE 2025 Gustavo Amorim Santos Faculty of Engineering, University of Porto, Alexandra Mendes Faculty of Engineering, University of Porto & INESC TEC, João Bispo Faculdade de Engenharia e Universidade do Porto Pre-print |