Abstract Acceleration of General Linear Loops

Résumé : Nous présentons une technique d'accélération pour calculer des invariants de boucles de programmes numériques avec affectations et conditions de boucle linéaires. Tandis que les techniques d'interprétation abstraite classiques sur-approximent l'ensemble des états accessibles par un calcul itératif, l'accélération abstraite capture l'effet d'une boucle avec une fonction de transfert non itérative appliquée aux états initiaux en tête de boucle. Comparé aux techniques d'accélération antérieures, celle-ci s'applique à des boucles linéaires quelconques sans autre restriction. La nouveauté de l'approche réside dans l'utilisation de la forme normale de Jordan de la matrice modélisant le corps de boucle, et de la dérivation d'expressions symboliques pour les entrées de la matrice modélisant l'effet de n>=0 itérations de boucle. Ces expressions font intervenir n à travers des fonctions polynomiales, exponentielles, et trigonométriques. C'est pourquoi nous introduisons un domaine abstrait pour les matrices qui capture les inégalités linéaires satisfaites par ces expressions symboliques. On obtient ainsi une matrice abstraite décrivant la sémantique de point-fixe de la boucle. Cette approche s'intègre facilement dans un interprète abstrait standard et peut traiter des programmes avec des boucles imbriquées ou contenant des branchements conditionnels. Nous l'avons évaluée sur des boucles simples mais au comportement complexe couramment rencontrées dans des programmes de contrôle-commande, et l'avons comparée à d'autres outils calculant des invariants de boucles linéaires. Les boucles considérées ont typiquement des comportements polynômiaux, exponentiels et oscillatoires, qui représentent un défi pour les approches existantes. Notre technique infère des invariants non triviaux permettant de prouver des bornes "utiles" sur les variables de ces boucles; elle surpasse clairement les approches existantes en termes de précision, tout en ayant de bonnes performances en terme de temps d'exécution.
Type de document :
Autre publication
Extended version of the POPL'14 paper. 2013
Liste complète des métadonnées

https://hal.inria.fr/hal-00924264
Contributeur : Bertrand Jeannet <>
Soumis le : lundi 6 janvier 2014 - 15:45:03
Dernière modification le : mercredi 27 juillet 2016 - 14:48:48

Identifiants

  • HAL Id : hal-00924264, version 1
  • ARXIV : 1311.0768

Collections

Citation

Bertrand Jeannet, Peter Schrammel, Sriram Sankaranarayanan. Abstract Acceleration of General Linear Loops. Extended version of the POPL'14 paper. 2013. 〈hal-00924264〉

Partager

Métriques

Consultations de la notice

111