Les syst mes dynamiques hybrides sont des syst mes dynamiques faisant intervenir explicitement et simultan ment des ph nom nes ou des mod les de type dynamique continu et v nementiel. Dans cette th se, nous proposons des techniques algorithmiques de v rification formelle de propri t s pour ces syst mes. Ces techniques de v rification se basent sur le calcul de l'espace atteignable partir d'une r gion initiale pour d terminer si l'intersection de cet espace avec le domaine viter est bien vide. Notre m thode consiste partitionner l'espace d' tat du syst me complexe en r gions et approximer pour chacune de ces r gions la dynamique du syst me tudi par une dynamique plus simple. Nous pr sentons des extensions une proposition pr c dente afin de prendre en compte des incertitudes dans les dynamiques affines. Dans un premier temps cette incertitude est consid r e comme invariante. Dans un second temps nous la consid rons variante. Cette deuxi me extension permet de consid rer l'atteignabilit des syst mes non-lin aires.