Correctness-by-Construction for Feature-Oriented Software Product Lines
summary
Claims a construction method that computes relevant feature sequences for both original and variational method calls, defines CBC refinement rules for them, and composes contracts (using Thüm et al.’s explicit contracting) so proofs rely only on contracts. Implements the approach as VarCorC (Eclipse/Graphiti/EMF) that emits proof obligations for KeY and uses FeatureIDE for feature models; example push/sorted yields two proof files and KeY discharges both (green), demonstrating the toolchain works on the running example.
AI-written summary · about
chapters (6)
- 0:00Introduction
- 0:47FeatureOriented Programming
- 2:43CorrectnessbyConstruction
- 4:40Combination
- 8:26Refinement Rule
- 11:02Contract Composition
related talks
20mUnifying compositional verification and certified compilation with a three-dimensional(…)
15mLeveraging Relational Concept Analysis for Automated Feature Location in Software Product Lines
21mMechanised Hypersafety Proofs about Structured Data
20mA Modular Approach to Metatheoretic Reasoning for Extensible Languages
01h 09mPlenary: Neighborhoods Banding Together: Reasoning Globally about Programs
01h 00mCooperative Verification: Towards Reliable Safety-Critical Systems
28mX-by-Construction: Towards Ensuring Non-Functional Properties in by-Construction(…)
46mKeynote: Formal Verification? No, Formal Reasoning!