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 possède 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. C'est pourquoi nous proposons dans cet article un nouveau système déductif où l'exécution symbolique de programmes devient une règle pour la construction de preuves. 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.