Tabea Bordis

Context: Correctness-by-Construction (CbC) is a method for software development. In this process, programs are contracted and created through correctness-preserving refinements. Software product lines (SPLs) are used to manage a set of program variants. The VarCorC tool offers the possibility to develop SPLs using CbC.

Problem: Two approaches to product line verification are currently implemented in VarCorC: A product-based and a family-based approach. In comparable verification approaches, family-based approaches are usually more efficient. In a previous thesis, it was evaluated that this is not the case for the implemented approach in VarCorC. However, potential for optimization was evident.

Goal: Investigate the reasons for this and optimize the existing approach and evaluate the optimization.

Prerequisite: Programming knowledge in Java, basic knowledge in the area of program verification and specification.