Abstract-Software produktlinjeteknik syftar till en effektiv utveckling av programvarianter som delar en gemensam uppsättning funktioner och som skiljer sig åt i andra funktioner. Produktlinjer kan utvecklas effektivt med hjälp av funktionsorienterad programmering. Med tanke på ett funktionsval och koden artefakter för varje funktion, kan programvarianter genereras automatiskt. Kvaliteten på programvarianterna kan noggrant säkerställas genom formell verifiering. Verifiering av alla programvarianter kan dock vara dyrt och inkludera överflödiga verifieringsuppgifter. Vi inför en klassificering av befintliga metoder för verifiering av programvaras produktlinje och föreslår en korrekt sammansättning som ett nytt tillvägagångssätt. Bevis sammansättning genererar korrekthet bevis för varje program variant baserat på partiella bevis för varje funktion. Vi presenterar en fallstudie för att utvärdera bevissammansättningen och visa att den minskar ansträngningen för verifiering.
I REF föreslås en funktions- och produktbaserad verifieringsmetod för beteendeprogramegenskaper där för varje funktionsmodul ett partiellt bevisskript för Coq skapas manuellt.
Proof Composition for Deductive Verification of Software Product Lines
{'venue': '2011 IEEE Fourth International Conference on Software Testing, Verification and Validation Workshops', 'journal': '2011 IEEE Fourth International Conference on Software Testing, Verification and Validation Workshops', 'mag_field_of_study': ['Computer Science']}