Computing Invariants with Transformers: Experimental Scalability and Accuracy

Abstract : Using abstract interpretation, invariants are usually obtained by solving iteratively a system of equations linking preconditions according to program statements. However, it is also possible to abstract first the statements as transformers, and then propagate the preconditions using the transformers. The second approach is modular because procedures and loops can be abstracted once and for all, avoiding an iterative resolution over the call graph and all the control flow graphs. However, the transformer approach based on polyhedral abstract domains encurs two penalties: some invariant accuracy may be lost when computing transformers, and the execution time may increase exponentially because the dimension of a transformer is twice the dimension of a precondition. The purposes of this article are 1) to measure the benefits of the modular approach and its drawbacks in terms of execution time and accuracy using significant examples and a newly developed benchmark for loop invariant analysis, ALICe, 2) to present a new technique designed to reduce the accuracy loss when computing transformers, 3) to evaluate experimentally the accuracy gains this new technique and other previously discussed ones provide with ALICe test cases and 4) to compare the executions times and accuracies of different tools, ASPIC, ISL, PAGAI and PIPS. Our results suggest that the transformer-based approach used in PIPS, once improved with transformer lists, is as accurate as the other tools when dealing with the ALICe benchmark. Its modularity nevertheless leads to shorter execution times when dealing with nested loops and procedure calls found in real applications.
Type de document :
Communication dans un congrès
Liste complète des métadonnées

Littérature citée [26 références]  Voir  Masquer  Télécharger

https://hal-mines-paristech.archives-ouvertes.fr/hal-01058298
Contributeur : Claire Medrala <>
Soumis le : mardi 26 août 2014 - 15:09:27
Dernière modification le : vendredi 12 avril 2019 - 10:20:07
Document(s) archivé(s) le : jeudi 27 novembre 2014 - 16:12:51

Fichier

A-565.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Identifiants

Citation

Vivien Maisonneuve, Olivier Hermant, François Irigoin. Computing Invariants with Transformers: Experimental Scalability and Accuracy. Fifth International Workshop on Numerical and Symbolic Abstract Domains, Sep 2014, Munich, Germany. 14 p., Pages 17-31, ⟨10.1016/j.entcs.2014.08.003⟩. ⟨hal-01058298⟩

Partager

Métriques

Consultations de la notice

226

Téléchargements de fichiers

217