Automatic Verification of Integer Array Programs

We 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 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 SIL may be checked as entailment is decidable for SIL.

• Type: Conference
• Year: 2009
• Where: CAV
• Authors: Filip Konecný, Marius Bozga, Peter Habermehl, Radu Iosif, Tomás Vojnar
• Keywords: CAV 2009, Formal Methods, Integer Arrays, Priori Bounded Length, Syntactical Level--to Transducers