Abstracting Linear Programs with Arrays into Linear Programs
Alessandro Armando, Massimo Benerecetti, Jacopo Mantovani · 2005
We introduce a counterexample guided abstraction and refinement procedure for linear programs with arrays. Our procedure starts by abstracting away all array elements from the initial program and then it incrementally refines the abstract program by including array elements as suggested by the refinement process. While, in the worst case, the procedure may lead to the generation and analysis of the abstract program obtained by considering all the array elements of the concrete program, in many cases of interests only a few array elements suce to successfully conclude the analysis. This is unlike other approaches in which the complexity of the analysis always increases with the size of the arrays involved in the input program. Moreover our analysis of arrays is precise, unlike other approaches that trade precision for eciency and therefore may return false negatives.