ALICe: A Framework to Improve Affine Loop Invariant Computation

Abstract : A crucial point in program analysis is the computation of loop invariants. Accurate invariants are required to prove properties on a program but they are difficult to compute. Extensive research has been carried out but, to the best of our knowledge, no benchmark has ever been developed to compare algorithms and tools. We present ALICe, a toolset to compare automatic computation techniques of affine loop scalar invariants. It comes with a benchmark that we built using 102 test cases which we found in the loop invariant bibliography, and interfaces with three analysis programs, that rely on different techniques: Aspic, ISL and PIPS. Conversion tools are provided to handle format heterogeneity of these programs. Experimental results show the importance of model coding and the poor performances of PIPS on concurrent loops. To tackle these issues, we use two model restructurations techniques whose correctness is proved in Coq, and discuss the improvements realized.
Type de document :
Communication dans un congrès
Liste complète des métadonnées

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

https://hal-mines-paristech.archives-ouvertes.fr/hal-01086957
Contributeur : Claire Medrala <>
Soumis le : mardi 25 novembre 2014 - 11:51:45
Dernière modification le : lundi 12 novembre 2018 - 11:02:15
Document(s) archivé(s) le : jeudi 26 février 2015 - 11:10:50

Fichier

A-563.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01086957, version 1

Citation

Vivien Maisonneuve, Olivier Hermant, François Irigoin. ALICe: A Framework to Improve Affine Loop Invariant Computation . the 5th International Workshop on Invariant Generation (WING 2014), Jul 2014, Vienne, Austria. ⟨hal-01086957⟩

Partager

Métriques

Consultations de la notice

226

Téléchargements de fichiers

155