This thesis enters in the frame of the automatic verification of concurrent software based on an intermediary formal language : high-level colored Petri nets. We particularly endeavor to tackle the combinatorial explosion phenomenon induced by exhaustive exploration of all possible inter leavings of a system. We focus on taking advantage of the amount of memory and computing resources provided by a local network of workstations working cooperatively. For more efficiency, distribution of the system accessibility graph is based upon a structural analysis of the model. We also aim at preserving in this distributed environment the other techniques that try to limit the combinatorial explosion. We especially relax constraints on the graph exploration consistency. These approaches have then been validated and evaluated with our distributed and multithreaded model checker.
