Alexander Kittelmann

Context: There exist numerous approaches for deductively verifying software product lines. However, efficiently verifying features of product lines subject to evolution is a open problem. We developed a two-phased feature-family-based approach to address this challenge, but results were surprisingly bad. Problems could be: too small case study, bugs in the implementation, inherent proving overhead of the used tooling (KeY). 

Goal: Inspect and improve the current approach (concept and implementation). Develop a new case study from scratch and conduct a comprehensive  empirical evaluation.

Prerequisites: Basic knowledge of Java/JML, Design-by-Contract, product lines.