Abstract Acceleration of General Linear Loops - Archive ouverte HAL Access content directly
Other Publications Year : 2013

Abstract Acceleration of General Linear Loops

(1) , (2) , (3)
1
2
3

Abstract

We present abstract acceleration techniques for computing loop invariants for numerical programs with linear assignments and conditionals. Whereas abstract interpretation techniques typically over-approximate the set of reachable states iteratively, abstract acceleration captures the effect of the loop with a single, non-iterative transfer function applied to the initial states at the loop head. In contrast to previous acceleration techniques, our approach applies to any linear loop without restrictions. Its novelty lies in the use of the Jordan normal form decomposition of the loop body to derive symbolic expressions for the entries of the matrix modeling the effect of n>=0 iterations of the loop. The entries of such a matrix depend on $n$ through complex polynomial, exponential and trigonometric functions. Therefore, we introduces an abstract domain for matrices that captures the linear inequality relations between these complex expressions. This results in an abstract matrix for describing the fixpoint semantics of the loop. Our approach integrates smoothly into standard abstract interpreters and can handle programs with nested loops and loops containing conditional branches. We evaluate it over small but complex loops that are commonly found in control software, comparing it with other tools for computing linear loop invariants. The loops in our benchmarks typically exhibit polynomial, exponential and oscillatory behaviors that present challenges to existing approaches. Our approach finds non-trivial invariants to prove useful bounds on the values of variables for such loops, clearly outperforming the existing approaches in terms of precision while exhibiting good performance.
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.

Dates and versions

hal-00924264 , version 1 (06-01-2014)

Identifiers

Cite

Bertrand Jeannet, Peter Schrammel, Sriram Sankaranarayanan. Abstract Acceleration of General Linear Loops. 2013, pp.1-18. ⟨hal-00924264⟩
99 View
0 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More