Nous proposons un cadre général pour l'exécution symbolique de programmes écrits dans des langages munis de sémantiques formelles définies par réécriture de termes. Partant d'une définition d'un langage $\cal L$, on construit automatiquement la définition d'un nouveau langage ${\cal L}^{\it sym}$ qui a la même syntaxe que $\cal L$ mais qui étend les types de données de $\cal L$ avec des valeurs symboliques, et dont les régles sémantiques sont adaptées pour traiter les valeurs symboliques. L'exécution symbolique des programmes de $\cal L$ est alors définie comme l'exécution habituelle des programmes de ${\cal L}^{\it sym}$, c'est á dire, l'application des régles de la sémantique de ${\cal L}^{\it sym}$ aux programmes de $\cal L$ plongés dans ${\cal L}^{\it sym}$. Nous démontrons que l'exécution symbolique posséde les propriétés attendues, et illustrons l'approche sur un langage impératif simple défini dans la \emph{$\mathbb{\K}$ framework}. Nous présentons également un prototype de moteur symbolique implémenté en $\mathbb{\K}$.