Implémentation du domaine asbtrait numérique TVPI pour APRON

Abdellatif Atki 1, 2
2 ABSTRACTION - Abstract Interpretation and Static Analysis
CNRS - Centre National de la Recherche Scientifique : UMR 8548, Inria Paris-Rocquencourt, DI-ENS - Département d'informatique de l'École normale supérieure
Résumé : Ce document étend le travail effectué par Simon, King, et M. Howe et propose une implémentation du domaine abstrait numérique relationnel TVPI (Two Variables Per Inequality) dans la bibliothèque APRON. Ce domaine permet d'exprimer des invariants de la forme ax + by ≤ c pour a, b, et c quelconques. L'intérêt de son implémentation réside dans son rapport coût/précision convenable. Ce dernier est dû à sa représentation avantageuse sur machine, au coût relativement modeste de ses opérations, et aussi à certains outils algorithmiques et géométriques spécifiques au cas de deux variables par inégalité. Dans l'implémentation, nous avons eu à traiter certains points qui n'ont pas été décrits en détail dans Simon, King, et Howe, ainsi que de faire des choix techniques afin de respecter la complexité prouvée pour le TVPI. Nous avons aussi eu à faire des choix d'approximations pour implémenter les opérations de test et d'affectation (deux opérations de base dans un analyseur statique) dans le cas où le nombre de variables dans une expression linéaire est supérieur à deux.
Type de document :
Mémoires d'étudiants -- Hal-inria+
Performance et fiabilité [cs.PF]. 2013
Liste complète des métadonnées

https://hal.inria.fr/hal-00925999
Contributeur : Antoine Miné <>
Soumis le : mercredi 8 janvier 2014 - 23:37:00
Dernière modification le : vendredi 25 mai 2018 - 12:02:05

Identifiants

  • HAL Id : hal-00925999, version 1

Collections

Citation

Abdellatif Atki. Implémentation du domaine asbtrait numérique TVPI pour APRON. Performance et fiabilité [cs.PF]. 2013. 〈hal-00925999〉

Partager

Métriques

Consultations de la notice

213