Optimization of the verification of correctness-by-construction product lines in the tool VarCorC
- Type:Master's thesis
- Person in Charge:Open
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.