en vue de l’obtention du grade de Docteur en Sciences,

Classical model-checking tools verify concurrent programs under the tra-ditional Sequential Consistency (SC) memory model, in which all accesses to the shared memory are immediately visible globally, and where model-checking consists in verifying a given property when exploring the state space of a program. However, modern multi-core processor architectures implement relaxed memory models, such as Total Store Order (TSO), Par-tial Store Order (PSO), or an extension with locks such as x86-TSO, which allow stores to be delayed in various ways and thus introduce many more possible executions, and hence errors, than those present in SC. Of course, one can force a program executed in the context of a relaxed memory system to behave exactly as in SC by adding synchronization operations after every memory access. But this totally defeats the performance advantage that is precisely the motivation for implementing relaxed memory models instead of SC. Thus, when moving a program to an architecture implementing a re