Software product line (SPL) engineering is a well-known approach to
develop industry-size adaptable software systems. SPL are often used in
domains where high-quality software is desirable; the overwhelming
product diversity, however, remains a challenge for assuring
correctness. In this paper, we present delta-oriented slicing, an
approach to reduce the deductive verification effort across an SPL where
individual products are Java programs and their relations are described
by deltas. On the specification side, we extend the delta language to
deal with formal specifications. On the verification side, we combine
proof slicing and similarity-guided proof reuse to ease the verification
process.