Modularizing Theorems for Software Product Lines

A goal of software product lines is the economical synthesis of programs in a family of programs. In this paper, we explain how theorems about program properties can be integrated into feature-based development of software product lines. As a case study, we analyze an existing Java/JVM compilation correctness proof for defining, interpreting, compiling, and executing bytecode for the Java language. We explain how features modularize both programs and theorems. By composing features, the source code and theorems for a program are synthesized. Generated theorems may then be certified manually or automatically using a proof checker, opening a new line of research in verification.