Publication Details
Automatic Verification of Integer Array Programs
IOSIF, R.; KONEČNÝ, F.; VOJNAR, T.; HABERMEHL, P.; BOZGA, M. Automatic Verification of Integer Array Programs. TR-2009-2, Grenoble: VERIMAG, 2009. p. 0-0.
Czech title
Automatická verifikace programů s poli
Type
report
Language
English
Authors
Radu Iosif
Konečný Filip, Ing., Ph.D.
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)
Habermehl Peter
Bozga Marius
Konečný Filip, Ing., Ph.D.
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)
Habermehl Peter
Bozga Marius
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}.
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
BibTeX
@techreport{BUT192689,
author="Iosif {Radu} and Filip {Konečný} and Tomáš {Vojnar} and Peter {Habermehl} and Marius {Bozga}",
title="Automatic Verification of Integer Array Programs",
year="2009",
publisher="VERIMAG",
address="TR-2009-2, Grenoble",
pages="49",
url="http://www-verimag.imag.fr/TR/TR-2009-2.pdf"
}