Publication detail

Automatic Verification of Integer Array Programs

IOSIF, R. KONEČNÝ, F. VOJNAR, T. HABERMEHL, P. BOZGA, M.

Original Title

Automatic Verification of Integer Array Programs

English Title

Automatic Verification of Integer Array Programs

Type

conference paper

Language

en

Original Abstract

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

English abstract

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

Keywords

formal verification, arrays, automata, mathematical logic

RIV year

2009

Released

23.06.2009

Publisher

Springer Verlag

Location

Berlin

ISBN

978-3-642-02657-7

Book

Computer Aided Verification

Edition

Lecture Notes in Computer Science

Edition number

NEUVEDEN

Pages from

157

Pages to

172

Pages count

16

URL

Documents

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