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

ALICe: A Framework to Improve Affine Loop Invariant Computation

(1) , (1) , (1)
1
Vivien Maisonneuve
  • Fonction : Auteur
  • PersonId : 961759
Olivier Hermant
François Irigoin

Résumé

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)
Loading...

Dates et versions

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

Identifiants

  • HAL Id : hal-01086957 , version 1

Citer

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

Partager

Gmail Facebook Twitter LinkedIn More