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 cela 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. Nous montrons que l'on peut utiliser une méthode générique d'exécution symbolique de programmes, que nous avons introduite récemment, comme une stratégie de construction de preuves dans ce système déductif. Nous montrons que, moyennant des conditions raisonnables sur la sémantique des langages de programmation, notre méthode de vérification est correcte. 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.