Les procédures de décision se trouvent au coeur de tous les outils modernes de l'analyse et la vérification des programmes car leur utilisation accroît d'une part l'efficacité du système de vérification et décharge d'autre part l'utilisateur de l'interaction, souvent fastidieuse, avec le système. Néanmoins, la plupart des problèmes de vérification font intervenir des mélanges de différentes théories par exemples les listes, les tableaux et les réels. Pour résoudre ce genre de problème il est fort souhaitable de procéder de façon modulaire en faisant coopérer les procédures de décision connues sur les théories élémentaires. Cette direction de recherche a été explorée pour la première fois il y a une vingtaine d'années grâce à des travaux précurseurs concernant la combinaison disjointe menés indépendamment par Shostak d'une part et Nelson-Oppen d'autre part dans le cadre de la vérification des programmes. Nos objectifs dans le cadre du stage concernent d'une part, la reformulation dans un cadre plus uniforme de la combinaison des deux approches Nelson-Oppen et Shostak et d'autre part, la proposition des nouvelles procédures de combinaisons dans différents contextes spécifiques, par exemple la combinaison des théories de Shostak et les théories stable-infinies. Nous abordons par la suite le problème de combinaison non-disjointe en présentant les travaux préliminaires menés par Ringeissen-Tinelli et par Zarba . Nous réalisons également une expérimentation dans le système de vérification haRVey développé au sein de l'équipe Cassis.