Advisors:

Software product lines are used for highly efficient development of software products with a common code base. As they are used increasingly often in safety-critical sys-tems, means of verification have come into focus of research, but efficient verifications of software product lines are still a challenge. To verify a software product lines all its products need to be verified. Different approaches have emerged that try to accom-plish this. In this thesis, we revisit the discussion about benefits and weaknesses of the different approaches, with a focus on product line evolution. In product-based verifi-cation approaches, all products are generated and verified individually, which becomes infeasible with an increasing number of products. To solve this issue, in family-based theorem proving, a single metaproduct is generated that incorporates the variability of the whole product line. This approach, however, may cause problems because even for small changes in a single feature, the verification must be repeated completely. Feature-based approaches address this issue by verifying features in isolation, but as features regularly interact with each other, solely feature-based cannot be realized