Automatic Verification of Integer Array Programs

Overview & Synopsis

We provide a verification technique for a class of programs working on integerarrays of finite, but not a priori bounded length. We use the logic of integer arrays SIL\cite{lpar08} 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 pre-conditions derived during the computation in SIL are converted into counter automata (CA). Loops are automatically translated---purely on the syntactical level---to transducers. Pre-condition 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 may be checked as entailment is decidable for SIL.