Technical report

BOZGA Marius, HABERMEHL Peter, IOSIF Radu, KONEČNÝ Filip and VOJNAR Tomáš. Automatic Verification of Integer Array Programs. TR-2009-2, Grenoble: VERIMAG, 2009.
Publication language:english
Original title:Automatic Verification of Integer Array Programs
Title (cs):Automatická verifikace programů s poli
Place:TR-2009-2, Grenoble, FR
formal verification, arrays, automata, mathematical logic
This report is the full version of an CAV'09 paper. 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}.
   author = {Marius Bozga and Peter Habermehl and Radu Iosif
	and Filip Kone{\v{c}}n{\'{y}} and
	Tom{\'{a}}{\v{s}} Vojnar},
   title = {Automatic Verification of Integer Array Programs},
   pages = 49,
   year = 2009,
   location = {TR-2009-2, Grenoble, FR},
   publisher = {VERIMAG},
   language = {english},
   url = {}

Your IPv4 address:
Switch to https