Deciding extension of the theory of arrays by integrating decision procedures and instantiation strategies. Rapporto Interno DSI 309-06, Università degli Studi di

The theory of arrays read(write(a, i,e), i) = e i 6 = j → read(write(a, i,e), j) = read(a, j) ∀i.(read(a, i) = read(b, i)) → a = b Not sufficient for program verification problems as many papers have pointed out, e.g. [Suzuki & Jefferson (1980)] dealt with a predicate for recognizing sorted arrays But also, what about a dimension of arrays? This is tricky since the three axioms above allow arrays to be unbounded! Ghilardi et al. (UNIMI & INRIA-Lorraine) Deciding Extensions of the Theory of Arrays PDPAR 2006 2 / 2