http://mw.hh.se/wg211/index.php?action=history&feed=atom&title=WG211%2FM10SchaeferWG211/M10Schaefer - Revision history2026-04-05T20:55:54ZRevision history for this page on the wikiMediaWiki 1.43.5http://mw.hh.se/wg211/index.php?title=WG211/M10Schaefer&diff=53&oldid=prevAdmin: 1 revision2011-12-12T10:06:24Z<p>1 revision</p>
<p><b>New page</b></p><div>[[Category:WG211]]<br />
<br />
<br />
<br />
<strong>Deductive Verification of Software Product Lines</strong> by Ina Schaefer<br />
<br />
A software product line consists is a family of program variants that <br />are developed from a common code base. In particular, for <br />safety-critical or business-critical applications, product quality and <br />correctness has to be rigorously ensured. Analyzing each product variant <br />in isolation is in general infeasible, since the number of product <br />variants is exponential in the number of product features.<br /><br />In my talk, I present efficient deductive program verification <br />techniques for delta-oriented software product lines. Delta-oriented <br />programming is a modular, yet flexible way to describe a family of <br />program variants. Besides type-safety of delta-oriented product lines, <br />our verification techniques consider functional correctness properties <br />specified using design-by-contract. If product variability is restricted <br />suitably, compositional family-based verification can establish <br />correctness of all product variants by analyzing the product line code <br />base only once. Without any restrictions on product variability, <br />incremental product-based verification techniques reduce verification <br />effort by progressing from one verified program variant to the next. In <br />between both extrems, constraint-based verification techniques provide a <br />compromise between the family-based and product-based verification <br />approaches and allow relaxing the restrictions on the admissible product <br />variability.</div>Admin