Discovering Properties about Arrays in Simple Programs

  • Mathias Peron | Verimag Laboratory (France)

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

Speaker Details

Mathias Péron is finishing his PhD at Verimag laboratory (France), under the supervision of N. Halbwachs. His research interests are among abstract interpretation and static analysis of numerical programs. In particular he worked on handling disequality properties and array contents properties.

Watch Next