Optimization of the verification of correctness-by-construction product lines in the tool VarCorC

  • Type:Master's thesis
  • Supervisor:

    Tabea Bordis

  • 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.