L'interprétation abstraite recourt traditionnellement au widening pour assurer la terminaison du calcul de point-fixe en présence d'itérations ou de récursions non bornées.

Une technique alternative est l'accélération, qui consiste à calculer exactement et en un seul coup l'effet d'un nombre non bornée d'itérations d'une boucle. Dans le cadre de programmes manipulant des nombres, cette technique a été implémentée principalement pour la logique de Presburger. Par ailleurs, elle se limite à certains types de boucles simples et ne garantit pas la convergence du calcul de point-fixe.

Plus récemment, Gonnord et Halbwachs ont introduit en 2007 le concept d'accélération abstraite, qui consiste à approximer dans le domaine abstrait considéré le résultat exact d'un nombre d'itération quelconque d'une boucle. Ceci permet de combiner accélération et widening.

Les travaux de Gonnord et Halbwachs ne s'appliquent qu'à des automates purement numériques: les Booléens éventuels sont codés dans l'automate, ce qui pose des problèmes d'explosion combinatoire. Dans le but d'appliquer l'accélération abstraite à des programmes flôt de données synchrones (typiquement en LUSTRE), nous montrons

• d'une part comment étendre l'accélération à des systèmes avec entrées numériques
• et d'autre part comment l'appliquer efficacement sur des systèmes manipulant des variables numériques ET booléennes.