The Arithmetic-Geometric Progression Abstract Domain

Abstract : We present a new numerical abstract domain. This domain automatically detects and proves bounds on the values of program variables. For that purpose, it relates variable values to a clock counter. More precisely, it bounds these values with the i-th iterate of the function [X |-> aX+b] applied on M, where i denotes the clock counter and the floating-point numbers a, b, and M are discovered by the analysis. Such properties are especially useful to analyze loops in which a variable is iteratively assigned with a barycentric mean of the values that were associated with the same variable at some previous iterations. Because of rounding errors, the computation of this barycenter may diverge when the loop is iterated forever. Our domain provides a bound that depends on the execution time of the program.
Type de document :
Communication dans un congrès
Cousot, Radhia. the 6th International Conference on Verification, Model Checking and Abstract Interpretation - VMCAI 2005, Jan 2005, Paris, France. Springer, 3385, pp.42-58, 2005, Lecture Notes in Computer Science. 〈10.1007/978-3-540-30579-8_3〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00528450
Contributeur : Jérôme Feret <>
Soumis le : jeudi 21 octobre 2010 - 17:15:44
Dernière modification le : mardi 24 avril 2018 - 17:20:10

Lien texte intégral

Identifiants

Collections

Citation

Jérôme Feret. The Arithmetic-Geometric Progression Abstract Domain. Cousot, Radhia. the 6th International Conference on Verification, Model Checking and Abstract Interpretation - VMCAI 2005, Jan 2005, Paris, France. Springer, 3385, pp.42-58, 2005, Lecture Notes in Computer Science. 〈10.1007/978-3-540-30579-8_3〉. 〈inria-00528450〉

Partager

Métriques

Consultations de la notice

46