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

Type

article in a collection out of WoS and Scopus

Language

English

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

Keywords

formal verification, arrays, automata, mathematical logic

Authors

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

RIV year

2009

Released

23. 6. 2009

Publisher

Springer Verlag

Location

Berlin

ISBN

978-3-642-02657-7

Book

Computer Aided Verification

Edition

Lecture Notes in Computer Science

Pages from

157

Pages to

172

Pages count

16

URL

https://www.fit.vut.cz/research/publication/9005/

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",
  booktitle="Computer Aided Verification",
  year="2009",
  series="Lecture Notes in Computer Science",
  volume="5643",
  pages="157--172",
  publisher="Springer Verlag",
  address="Berlin",
  isbn="978-3-642-02657-7",
  url="https://www.fit.vut.cz/research/publication/9005/"
}