Verification of Software Product Lines: Reducing the Effort with Delta-oriented Slicing and Proof Reuse

@TechReport{BrunsKlebanovSchaefer10,
  author	= {Daniel Bruns and Vladimir Klebanov and Ina Schaefer},
  title		= {Verification of Software Product Lines: Reducing the
		   Effort with Delta-oriented Slicing and Proof Reuse},
  year		= 2010,
  month		= jun,
  address	= {Paris, France},
  booktitle	= {Papers Presented at the International Conference on Formal
		   Verification of Object-Oriented Software ({FoVeOOS} 2010)},
  editor	= {Bernhard Beckert and Claude March{\'e}},
  language	= {english},
  institution	= {Department of Informatics, Karlsruhe
		   Institute of Technology},
  series	= {Karlsruhe Reports in Informatics},
  number	= {2010-13},
  url		= {https://publikationen.bibliothek.kit.edu/1000019096},
  urn		= {urn:nbn:de:swb:90-190964},
  pages		= {345--358},
  abstract	= {Software product lines (SPL) are a well-known methodology
		   to develop industry-size adaptable software systems. SPL
		   are often used in domains where high-quality software is
		   desirable, but the overwhelming product diversity remains a
		   challenge for assuring correctness. We present our work in
		   progress on reducing the deductive verification effort
		   across different products of an SPL. On the specification
		   side, our approach enriches the delta language for
		   describing SPLs with formal product specifications. On the
		   verification side, we combine program slicing and
		   similarity-guided proof reuse to ease the verification
		   process.}
}