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