Systematic derivation of correct variability-aware program analyses

Jan Midtgaard, Aleksandar S. Dimovski, Claus Brabrand, Andrzej Wasowski

Research output: Contribution to journalJournal articleResearchpeer-review


A recent line of work lifts particular verification and analysis methods to Software Product Lines (SPL). In an effort to generalize such case-by-case approaches, we develop a systematic methodology for lifting single-program analyses to SPLs using abstract interpretation. Abstract interpretation is a classical framework for deriving static analyses in a compositional, step-by-step manner. We show how to take an analysis expressed as an abstract interpretation and lift each of the abstract interpretation steps to a family of programs (SPL). This includes schemes for lifting domain types, and combinators for lifting analyses and Galois connections. We prove that for analyses developed using our method, the soundness of lifting follows by construction. The resulting variational abstract interpretation is a conceptual framework for understanding, deriving, and validating static analyses for SPLs. Then we show how to derive the corresponding variational dataflow equations for an example static analysis, a constant propagation analysis. We also describe how to approximate variability by applying variability-aware abstractions to SPL analysis. Finally, we discuss how to efficiently implement our method and present some evaluation results.
Original languageEnglish
JournalScience of Computer Programming
Pages (from-to)145-170
Publication statusPublished - 2015


  • Abstract interpretation
  • Software Product Lines
  • Software variability
  • Static analysis
  • Verification
  • Abstracting
  • Computer software
  • Data flow analysis
  • Model checking
  • Abstract interpretations
  • Conceptual frameworks
  • Constant propagation
  • Software Product Line
  • Software product lines
  • Software variabilities
  • Systematic methodology
  • Verification and analysis

Fingerprint Dive into the research topics of 'Systematic derivation of correct variability-aware program analyses'. Together they form a unique fingerprint.

Cite this