Les systèmes informatiques sont devenus omniprésents dans notre vie quotidienne. Garantir la fiabilité et la robustesse de ces systèmes est une nécessité absolue. La Vérification de Modèles (Model-Checking) est l'une des approches dédiées à cette fin. Son objectif est de prouver l'absence de défaillances ou d'identifier d'éventuelles erreurs. La Vérification de Modèles se décline en plusieurs techniques. Parmi celles-ci, on trouve la Vérification de Modèles Bornée (Bounded Model Checking - BMC), une technique qui repose sur la satisfaisabilité booléenne (SAT). L'idée centrale derrière le BMC est de vérifier qu'un modèle, limité à des exécutions bornées par un entier k, satisfait sa spécification, souvent définie comme un ensemble d'expressions logiques temporelles. Dans cette approche, les comportements du système sont exprimés sous forme de problèmes SAT. Contrairement à d'autres méthodes de vérification formelle, le BMC basé sur SAT n'est généralement pas sensible au problème de l'explosion de l'espace d'états, ce qui peut poser problème lors de la conception de systèmes impliquant des millions de variables et de contraintes. Cependant, le compromis réside dans la complexité temporelle, car les problèmes SAT sont connus pour être NP-complets. Au cours des dernières décennies, d'importantes avancées ont été réalisées dans la résolution séquentielle de problèmes SAT. Ces développements se sont principalement concentrés sur l'utilisation d'informations dynamiques, acquises lors du processus de résolution (par exemple, l'apprentissage de clauses binaires) ou d'informations statiques, extraites de la structure inhérente du problème SAT (par exemple, la structure communautaire). Cependant, moins d'attention a été accordée aux informations structurelles intégrées dans le problème initial. Par exemple, lorsque qu'un problème BMC est réduit à SAT, des informations cruciales sont perdues dans la traduction. Comme le souligne cette thèse, la réintégration de ces informations perdues peut considérablement améliorer le processus de résolution. Ce travail explore des moyens d'améliorer la résolution de problèmes BMC basés sur SAT, tant dans des contextes séquentiels que parallèles, en exploitant et en valorisant les informations pertinentes extraites des caractéristiques inhérentes du problème. Cela peut impliquer l'amélioration d'heuristiques génériques existantes ou la décomposition efficace de la formule en partitions.