Verifying Software Product Lines with ProVeLines

National audienceSoftware Product Lines (SPLs) are families of similar software products built from a common set of features. As the number of products of an SPL is potentially exponential in the number of its features, SPLs are harder to verify than single software. A practical way to face this exponential blow-up is to reuse common behaviour between products. We previously introduced Featured Transition Systems (FTS), a mathematical model that serves as a basis for efficient SPL model checking techniques. In this talk, we present ProVeLines, a product line of verifiers for SPLs that incorporates the results of over three years of research on formal verification of SPLs. Being itself a product line, our tool is flexible and extensible, and offers a wide range of solutions for SPL modelling and verification. Its recently re-designed API allows for an easy integration of ProVeLines in development tools. During the talk, we illustrate how our model checker can be used during the development life cycle to generate verified code