Formalisation d'un vérificateur efficace d'assertions arithmétiques à l'exécution

Thibaut Benjamin (1) , Félix Ridoux (1, 2) , Julien Signoles (1)

1 LIST (CEA) - Laboratoire d'Intégration des Systèmes et des Technologies
2 ENS Rennes - École normale supérieure - Rennes

La vérification d'assertions à l'exécution est une technique consistant à vérifier la validité d'annotations formelles pendant l'exécution d'un programme. Bien qu'ancienne, cette technique reste encore peu étudiée d'un point de vue théorique. Cet article contribue à pallier ce manque en formalisant un vérificateur d'assertions à l'exécution pour des propriétés arithmétiques entières. La principale difficulté réside dans la modélisation d'un générateur de code pour les propriétés visées qui génère du code à la fois correct et efficace. Ainsi, le code généré repose sur des entiers machines lorsque le générateur peut prouver qu'il est correct de le faire et sur une bibliothèque spécialisée dans l'arithmétique exacte, correcte mais moins efficace, dans les autres cas. Il utilise pour cela un système de types dédié. En outre, la logique considérée pour les propriétés inclue des constructions d'ordre supérieur. L'article présente également une implémentation de ce générateur de code au sein d'E-ACSL, le greffon de Frama-C dédié à la vérification d'assertions à l'exécution, ainsi qu'une première évaluation expérimentale démontrant empiriquement l'efficacité du code généré.

Domaines: Informatique [cs]

Thibaut Benjamin, Félix Ridoux, Julien Signoles. Formalisation d'un vérificateur efficace d'assertions arithmétiques à l'exécution. 33èmes Journées Francophones des Langages Applicatifs, Jun 2022, Saint-Médard-d'Excideuil, France. pp.24-41. ⟨hal-03626779⟩