On Verifying Temporal Properties of Configurable Software

Configurable software systems today are becoming very popular. They can produce a set of related programs by choosing preferable features (configuration options) at compile-time. Many configurable programs are applied in safety-critical areas, so their formal verification is of primary importance. In this paper, we introduce a new, interesting approach for verifying temporal properties of configurable programs that contain numerical features. We extend an abstract interpretation-based static analysis framework for proving temporal properties of single programs that uses a decision tree abstract domain. In particular, we define a novel lifted decision tree domain for proving temporal properties of configurable programs. We have developed a lifted static analyzer for proving temporal properties of #if-enriched C configurable programs. The evaluation on a range of loop benchmarks from SV-COMP confirms the effectiveness of our approach.