Applications of First-order Integer Arithmetic to the Verification of Programs with Lists

The arithmetic of natural numbers with addition and divisibility has been shown undecidable as a consequence of the fact that multiplication of natural numbers can be interpreted into this theory, as shown by J. Robinson (1949). The most important decidable subsets of the arithmetic of addition and divisibility are the arithmetic of addition, proved by M. Presburger (1929), and the purely existential subset, proved independently by A. Beltyukov and L. Lipshitz (1976). In the first part of the talk, we will investigate the decidability of a new subset of the arithmetic with addition and divisibility, consisting of formulae with quantifier prefix in the language Q^* {∃, ∀}^*, Q ∈ {∃, ∀}, where the first Q-quantified variables are the variables occurring to the left of the divisibility predicate. The advantage of this subset is that it allows a limited form of quantifier alternation. In the second part of the talk, we will analyze the complexity of checking safety and termination properties, for a very simple, yet non-trivial, class of programs with singly-linked list data structures. Since, in general, programs with lists are known to have the power of Turing machines, we restrict the control structure, by forbidding nested loops and destructive updates. Surprisingly, even with these simplifying conditions, the class of programs working on heaps with more than one cycle has undecidable safety and termination problems, whereas decidability can be established when the input heaps may have at most one loop. The proofs for both the undecidability and the decidability results rely on the number-theoretic results presented previously. The talk extends some results presented at FOSSACS 2005 and is joint work with Marius Bozga (Verimag, F).