Discovering Properties about Arrays in Simple Programs

Опубликовано 6 сентября 2016, 17:25

These last five years we have seen a real advance on the static analysis of array contents. On the one hand, there is the work initiated by Flanagan and Qadeer in 2002, using predicate abstraction, possibly improved with counter-example guided refinement (Beyer et al, 2007). On the other hand, some abstract domains have emerged: in the work of Gopan, Reps and Sagiv in 2005, the domain is based on variables summarizing all cells of an array belonging to a predefined symbolic subpart (e.g. [1..i-1]); in the work of Gulwani, McCloskey and Tiwari in 2008, the domain is based on a conjunction of implications, where quantified variables, constrained by the antecedent formulas, index arrays in the consequent formulas (e.g. forall).