Cet article propose un nouvel outil, ACInv, pour relever les défis de la vérification automatisée de programmes, essentielle à la création de logiciels fiables, notamment lors de l'analyse de programmes réels avec des structures de données et un flux de contrôle complexes. ACInv génère des invariants de boucle en combinant l'analyse statique avec un modèle de langage à grande échelle (LLM). Il extrait les informations de boucle par analyse statique et les intègre dans l'invite LLM. Il utilise ensuite un évaluateur basé sur LLM pour vérifier les invariants générés et les renforcer, les affaiblir ou les rejeter afin d'obtenir des invariants optimaux. Les résultats expérimentaux montrent qu'ACInv surpasse les outils existants sur les ensembles de données contenant des structures de données, tout en conservant des performances comparables à celles de l'outil de pointe, AutoSpec, sur les programmes numériques sans structures de données. ACInv résout 21 % d'exemples de plus qu'AutoSpec sur l'ensemble des données et génère des modèles de structures de données de référence.
