List DILS vous invite à son événement

Séminaire LSL - Mamy Razafintsialonina - Réutilisations de caches et d’invariants pour l’analyse statique incrémentale

À propos de cet événement

Résumé

L’analyse statique de programmes permet aujourd’hui d’analyser des programmes de grande taille, avec une très bonne précision, tout en étant raisonnablement rapide. Néanmoins, les temps d’analyse continuent de se compter en minutes, voire dizaines de minutes, ce qui rend compliqué leur intégration dans les processus de développement : les modifications d’un programme y sont très fréquentes et requièrent donc d’obtenir rapidement les résultats de l’analyseur. Néanmoins, ces modifications sont souvent mineures, de l’ordre de quelques lignes de code tout au plus. L’analyse statique incrémentale exploite cette caractéristique pour permettre à un analyseur statique de se contenter d’actualiser les résultats d’une analyse antérieure plutôt que de tout recalculer, ce qui permet des gains de temps significatifs. Cet article présente deux nouvelles approches pour l’analyse statique incrémentale, l’une réutilisant des caches de fonction et l’autre des invariants de boucle. Nous les avons implémentées dans Eva, l’analyseur de valeurs par interprétation abstraite de Frama-C en utilisant une nouvelle fonctionalité de cette plateforme permettant de comparer deux programmes. Nos travaux ont été évalués sur un ensemble de commits de programmes réels.

Proposé par

  • Intervenant externe
    MR I
    Mamy Razafintsialonina

  • Intervenant externe
    MR I
    Mamy Razafintsialonina

List DILS

Le CEA est un organisme de recherche sur la défense et la sécurité, les énergies nucléaire et renouvelables, la recherche technologique pour l’industrie et la recherche fondamentale en sciences de la matière et de la vie.