Roland Herrmann
University of Regensburg, Germany
The theory of arrays, supported by virtually all SMT solvers, is one of the most important theories in program verification. The standard theory of arrays, which provides read and write operations, has been extended in various different ways in past research, among others, by adding extensionality, constant arrays, function mapping (resulting in combinatorial array logic), counting, and projections. However, sum constraints, which capture properties of the sum of all elements of an integer array are still missing. We investigate on the decidabiility of various theories with arrays. Combinatory array with sum constraints are shown to be undecidable, but leaving out mapping constraints retains decidability. We aim to provide a complete characterization of decidable and undecidable fragments with various decidability proofs of different flavour.