Industrial Grade Model Checking Use Cases, Constraints, Tools and Applications

International audienceModel checking has made a lot of progress since its infancy. For a long time, industrial applications were still limited to some very specific domains out of which the technique bumps into the state explosion wall. Nowadays things evolve and some tools are able to tackle real world use cases outside of the known domains. We give here the feedback collected when using model checking on several industrial strength use cases and give indication on how we take into account the specific domain constraints. 1 Model Checking for Industrial Problems Model checking refers to the problem of exhaustively and automatically checking whether a given model of a system meets a given specification. Model Checking is now an old technique which takes its ground in the mid 1970s as a response to concurrent problem analysis. It was until recently essentially confined to some specific areas, such as hardware analysis or protocol verification. Extension to other domains such as software verification has always been difficult due to the combinatorial explosion problem (the size of the space state grows exponentially with the size of the problem to analyze). However, recent developments in a variety of fields, ranging from symbolic model checking to SAT solver engines and including model checker parallelization lead to a broader range of application in industry including software analysis