Detail publikace
Automatic Verification of Integer Array Programs
IOSIF, R. KONEČNÝ, F. VOJNAR, T. HABERMEHL, P. BOZGA, M.
Originální název
Automatic Verification of Integer Array Programs
Anglický název
Automatic Verification of Integer Array Programs
Jazyk
en
Originální abstrakt
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}.
Anglický abstrakt
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}.
Dokumenty
BibTex
@inproceedings{BUT30759,
author="Iosif {Radu} and Filip {Konečný} and Tomáš {Vojnar} and Peter {Habermehl} and Marius {Bozga}",
title="Automatic Verification of Integer Array Programs",
annote="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}.",
address="Springer Verlag",
booktitle="Computer Aided Verification",
chapter="30759",
edition="Lecture Notes in Computer Science",
howpublished="print",
institution="Springer Verlag",
journal="Lecture Notes in Computer Science (IF 0,513)",
year="2009",
month="june",
pages="157--172",
publisher="Springer Verlag",
type="conference paper"
}