Systematic Derivation of Static Analyses for Software Product Lines

    Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review

    Abstract

    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
    Place of PublicationCopenhagen
    PublisherAssociation for Computing Machinery
    Publication dateMar 2014
    EditionTR-2014-170
    Pages181-192
    ISBN (Print)978-1-4503-2772-5
    ISBN (Electronic)978-87-7949-308-7
    DOIs
    Publication statusPublished - Mar 2014
    SeriesIT University Technical Report Series
    NumberTR-2014-170
    ISSN1600-6100

    Keywords

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

    Fingerprint

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

    Cite this