Verifying Evolving Product Lines with Uninterpreted Predicates
- Subject:Verifying Evolving Product Lines with Uninterpreted Predicates
- Type:Bachelor's thesis
- Supervisor:
- Person in Charge:Open
-
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.