Automatic Verification of Integer Array Programs

International audienceWe provide a verification technique for a class of programs working on integer arrays of finite, but not a priori bounded length. We use the logic of integer arrays SIL [13] to specify pre-and post-conditions of programs and their parts. Effects of non-looping parts of code are computed syntactically on the level of SIL. Loop preconditions derived during the computation in SIL are converted into counter automata (CA). Loops are automatically translated— purely on the syntactical level—to transducers. Precondition CA and transducers are composed, and the composition over-approximated by flat automata with difference bound constraints, which are next converted back into SIL formulae, thus inferring post-conditions of the loops. Finally, validity of post-conditions specified by the user in SIL may be checked as entailment is decidable for SIL