Maximilian Kodetzki, Tabea Bordis, Tobias Runge, Ina Schaefer
Technical Track
 | Haus der Universität, Schlösslistrasse 5, 3008 Bern, Switzerland |
 | 7 February 2024, 15:50 CET |
 | Maximilian Kodetzki |
 | Michael Franziskus Hönig |
 | https://dl.acm.org/doi/10.1145/3634713.3634714 |
Software product lines (SPLs) are a technique to efficiently develop families of software products. Code is implemented in functional features which are composed to individual software variants. SPLs are oftentimes used in safety-critical systems, which is why functional correctness is more important than ever. As an advanced approach, deductive verification offers the possibility to verify the behaviour of software against a formal specification. When deductive verification is applied for SPLs, it meets the challenges of an SPLs variability. Since most verification approaches do not scale for variant-rich product lines, we take up existing approaches of reuse of proof parts to develop our concept of partial proofs. We split proofs into a feature-specific and a product-specific part. The feature-specific part is only proven once for all products enabling advanced proof reuse. We implement our concept of partial proofs in the tool VarCorC and evaluate it on three case studies. We found that both the number of proof steps and the verification time can be reduced by using partial proofs. Further, we determine a trend of increasing improvements of verification costs for large-scale SPLs.