Avant d'exploiter ou de diffuser un logiciel, il convient de s'assurer de sa correction. Lorsque la taille du programme est grande, l'automatisation de la preuve est à rechercher, mais elle ne peut être une panacée (théorème de Rice). Ce rapport s'inscrit dans une étude utilisant les systèmes de réécriture (TRS) comme modèles formels des programmes : la correction s'exprime par le fait que l'ensemble des termes accessibles par le TRS considéré est disjoint d'un ensemble de termes représentant les mauvais comportements. On sait décider une telle propriété si les langages en jeu sont réguliers (au sens des automates d'arbres). Certaines classes de TRS préservant la régularité sont connues mais ne couvrent pas tous les cas. Ici, nous nous intéressons à la complétion d'automate. La complétion équationnelle permet de paramétrer la sur-approximation par un ensemble $E$ d'équations entre termes afin de favoriser l'obtention d'un point fixe. Nous exposons cette méthode et tentons de l'exprimer dans le vocabulaire de l'interprétation abstraite, une autre méthode d'élaboration d'analyses statiques.