Sciweavers

Share
FOSSACS
2008
Springer

What Else Is Decidable about Integer Arrays?

8 years 4 months ago
What Else Is Decidable about Integer Arrays?
We introduce a new decidable logic for reasoning about infinite arrays of integers. The logic is in the first-order fragment and allows (1) Presburger constraints on existentially quantified variables, (2) difference constraints as well as periodicity constraints on universally quantified indices, and (3) difference constraints on values. In particular, using our logic, one can express constraints on consecutive elements of arrays (e.g. i . 0 i < n a[i+1] = a[i]-1) as well as periodic facts (e.g. i . i 2 0 a[i] = 0). The decision procedure follows the automata-theoretic approach: we translate formulae into a special class of B
Peter Habermehl, Radu Iosif, Tomás Vojnar
Added 26 Oct 2010
Updated 26 Oct 2010
Type Conference
Year 2008
Where FOSSACS
Authors Peter Habermehl, Radu Iosif, Tomás Vojnar
Comments (0)
books