Model-checking techniques suffer from the state explosion problem that prevents them to scale up. During the past decades, researchers have been trying to alleviate the state explosion problem using various techniques like partial order reduction or symbolic data structures or abstractions.

Defined in my PhD thesis, I will present an abstraction based approach to solve the model-checking of safety properties. By using abstractions, we trade precision for tractability: the abstracted model-checking problem is ’easier’ to solve but its solution may be too imprecise to draw any conclusion on the original problem. In such a case, precision is recovered by refining the abstraction that is used. Iterating this process yields to increased precision and eventually a solution to the original problem. We will illustrate our approach through simple examples and conclude by giving an application of our approach to solve coverability problem for Petri nets. Our implementation of the above approach for Petri nets is the state of the art.

Our approach has been entirely formalized in the abstract interpretation framework which will be recalled at the beginning of the talk.