Génération automatique d'invariants de boucle et affinement par échantillonnage sélectif

La génération automatique d'invariants de boucle est importante dans l'analyse et la vérification des programmes. Dans cet article, nous proposons de générer automatiquement des invariants de boucle par apprentissage et vérification. Étant donné un triple de Hoare d'un programme contenant une boucle, nous commençons par tester aléatoirement le programme, collecter les états du programme en temps réel et les catégoriser en fonction de leur conformité avec l'invariant à découvrir. Ensuite, des techniques de classification sont utilisées pour générer automatiquement un candidat invariant de boucle. Par la suite, nous affinons le candidat par un échantillonnage sélectif afin de surmonter le manque de cas de test suffisants. Ce n'est qu'après qu'un invariant candidat ne peut plus être amélioré par échantillonnage sélectif que nous vérifions s'il peut être utilisé pour prouver le triple de Hoare. S'il ne peut pas, les contre-exemples générés sont ajoutés en tant que nouveaux tests et nous répétons le processus ci-dessus. De plus, nous montrons qu'en introduisant un apprentissage sensible aux chemins, c'est-à-dire en partitionnant les états du programme en fonction des emplacements du programme visités et en classant chaque partition séparément, nous sommes capables d'apprendre des invariants de boucle disjonctifs. Afin d'évaluer notre idée, un outil prototype a été développé et les résultats des expériences montrent que notre approche complète les approches existantes.