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"
}