Systematic Derivation of Static Analyses for Software Product Lines

Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-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 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. This includes schemes for how to lift 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. Finally, we discuss approximating variability in an analysis and we derive variational data-flow equations for an example analysis, a constant propagation analysis for a simple imperative language.
Original languageEnglish
Title of host publication MODULARITY '14 Proceedings of the 13th international conference on Modularity
Number of pages12
PublisherAssociation for Computing Machinery
Publication dateMar 2014
ISBN (Print)978-1-4503-2772-5
ISBN (Electronic)978-87-7949-308-7
Publication statusPublished - Mar 2014
SeriesITU Technical Report Series


  • Software product lines
  • verification
  • Static Analysis
  • Abstract Interpretation


Dive into the research topics of 'Systematic Derivation of Static Analyses for Software Product Lines'. Together they form a unique fingerprint.

Cite this