Nous proposons de nouveaux algorithmes et de nouvelles structures de données pour la vérification formelle de systèmes réactifs finis sur architectures parallèles. Ces travaux se basent sur les techniques de vérification par model-checking. Notre approche cible des architectures multi-processeurs et multi-coeurs, avec mémoire partagée, qui correspondent aux générations de serveurs les plus performants disponibles actuellement. Dans ce contexte, notre objectif principal est de proposer des approches qui soient à la fois efficaces au niveau des performances, mais aussi compatibles avec les politiques de partage dynamique du travail utilisées par les algorithmes de génération d'espaces d'états en parallèle, ainsi, nous ne plaçons pas de contraintes sur la manière dont le travail ou les données sont partagés entre les processeurs. Parallèlement à la définition de nouveaux algorithmes de model-checking pour machines multi-coeurs, nous nous intéressons également aux algorithmes de vérification probabiliste. Par probabiliste, nous entendons des algorithmes de model-checking qui ont une forte probabilité de visiter tous les états durant la vérification d'un système. La vérification probabiliste permet des gains importants au niveau de la mémoire utilisée, en échange d'une faible probabilité de ne pas être exhaustif, il s'agit donc d'une stratégie permettant de répondre au problème de l'explosion combinatoire.