  Safety-critical software systems are in many cases designed and implemented
as families of products, usually referred to as Software Product Lines (SPLs).
Products within an SPL vary from each other in terms of which features they
include. Applying existing analysis techniques to SPLs and their safety cases
is usually challenging because of the potentially exponential number of
products with respect to the number of supported features. In this paper, we
present a methodology and infrastructure for certified \emph{lifting} of
existing single-product safety analyses to product lines. To ensure certified
safety of our infrastructure, we implement it in an interactive theorem prover,
including formal definitions, lemmas, correctness criteria theorems, and
proofs. We apply this infrastructure to formalize and lift a Change Impact
Assessment (CIA) algorithm. We present a formal definition of the lifted
algorithm, outline its correctness proof (with the full machine-checked proof
available online), and discuss its implementation within a model management
framework.
