ALICe: A Framework to Improve Affine Loop Invariant Computation - Mines Paris Accéder directement au contenu
Communication Dans Un Congrès Année :

ALICe: A Framework to Improve Affine Loop Invariant Computation

Vivien Maisonneuve
  • Fonction : Auteur
  • PersonId : 961759
Olivier Hermant
François Irigoin


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.
Fichier principal
Vignette du fichier
A-563.pdf (266.94 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-01086957 , version 1 (25-11-2014)


  • HAL Id : hal-01086957 , version 1


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⟩
182 Consultations
170 Téléchargements


Gmail Facebook Twitter LinkedIn More