Publication Details

Automatic Verification of Integer Array Programs

BOZGA Marius, HABERMEHL Peter, IOSIF Radu, KONEČNÝ Filip and VOJNAR Tomáš. Automatic Verification of Integer Array Programs. TR-2009-2, Grenoble: VERIMAG, 2009.
Czech title
Automatická verifikace programů s poli
Type
technical report
Language
english
Authors
Bozga Marius (VERIMAG)
Habermehl Peter (UPAR7)
Iosif Radu (VERIMAG)
Konečný Filip, Ing. (DITS FIT BUT)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
URL
Keywords

formal verification, arrays, automata, mathematical logic

Abstract
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}.
Published
2009
Pages
49
Publisher
VERIMAG
Place
TR-2009-2, Grenoble, FR
BibTeX 
@TECHREPORT{FITPUB9006,
   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 = "https://www.fit.vut.cz/research/publication/9006"
}
Back to top