Formalisation d'un vérificateur efficace d'assertions arithmétiques à l'exécution
Abstract
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’EACSL, 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é.
Domains
Other
Origin : Files produced by the author(s)