A software product line is a set of systems with well-defined commonalities and variabilities that are developed by managed reuse. Because of the huge number of possible configurations, it is crucial to guarantee critical system requirements. However, it is infeasible to formally verify each system in isolation. Instead, verification artifacts, i.e., properties and their proofs, should be reused in same way as other development artifacts.

In this talk, I present to concept of proof reuse for the efficient verification of software product lines. The presented approach is based on delta-modeling, a general approach to capture feature-based variability of software product lines. A set of systems is represented by a core system and a set of system deltas modifying the core to capture other system features. The delta modeling structure can be exploited to determine the reuse potential for proofs of system properties. This will be illustrated at experiments with the KeY verification system.