Nous présentons une approche pour améliorer l'efficacité de l'analyse statique de programmes C, fondée sur l'incrémentalité et appliquée au greffon EVA de la plateforme Frama-C. Notre approche comprend deux techniques. La première est le résumé de fonction qui permet de réutiliser les résultats d'analyses sauvegardés pour des fonctions avec des entrées similaires. La seconde est la réutilisation d'invariants de boucle, qui permet d'accélérer l'analyse des boucles en commençant les itérations à partir des invariants précédemment inférés. Ce travail contribue au groupe de travail LVP du GDR GPL.

Groupe de travail : LVP