Detail publikace
Automatic Verification of Integer Array Programs
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}.
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"
}