Nous présentons une méthode automatique pour vérifier des programmes qui ne dépend pas du langage de programmation dans lequel les programmes à vérifier sont écrits. Pour celà nous nous appuyons sur la Reachability Logic, un formalisme de spécification introduit récemment, qui peut être vu comme une alternative à la logique de Hoare, mais qui, contrairement à cette dernière, ne dépend pas du langage de programmation utilisé. La Reachability Logic a un système déductif qui est correct et relativement complet, qui laisse beaucoup de liberté à l'utilisateur sur la manière d'appliquer les règles de déduction, mais qui n'offre pas de mode d'emploi pour construire des preuves. Par conséquent nous proposons ici un autre système déductif dans lequel l'exécution symbolique est utilisée pour la construction systématique de preuves. Nous montrons que, moyennant des conditions raisonnables sur la sémantique des langages de programmation et sur les propriétés des programmes, une certaine stratégie d'application des règles de notre système déductif est correcte et faiblement complète. Ceci dit en substance que, lorsqu'elle termine, notre stratégie résout le problème de vérification de programmes à base de Reachability Logic. Nous présentons une implémentation prototype d'un outil de vérification basé sur ces idées, que nous avons implémenté dans la K framework, et que nous illustrons sur des exemples de programmes écrits dans des langages formellement définis en K.