Verimag

Technical Reports

M. Bozga, P. Habermehl, R. Iosif, F. Konecny, and T. Vojnar
Automatic Verification of Integer Array Programs (2009)

TR-2009-2.pdf


Keywords: program verification, counter automata, array programs

Abstract: We provide a verification technique for a class of programs working on \emph{integer arrays} of finite,but not a priori bounded length. We use the logic of integer arrays \textbf{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 \textbf{SIL}. Loop pre-conditions derived during the computation in \textbf{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 \textbf{SIL} formulae, thus inferring post-conditions of the loops. Finally, validity of post-conditions specified by the user in \textbf{SIL} may be checked as entailment is decidable for \textbf{SIL}.

Contact | Plan du site | Site réalisé avec SPIP 3.0.26 + AHUNTSIC [CC License]

info visites 874884