Skip to Main content Skip to Navigation
Conference papers

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.
Complete list of metadata

Cited literature [42 references]  Display  Hide  Download

https://hal-mines-paristech.archives-ouvertes.fr/hal-01086957
Contributor : Claire Medrala <>
Submitted on : Tuesday, November 25, 2014 - 11:51:45 AM
Last modification on : Thursday, September 24, 2020 - 4:36:02 PM
Long-term archiving on: : Thursday, February 26, 2015 - 11:10:50 AM

File

A-563.pdf
Files produced by the author(s)

Identifiers

  • 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⟩

Share

Metrics

Record views

280

Files downloads

198