Publication Details

Automatic Verification of Integer Array Programs

BOZGA Marius, HABERMEHL Peter, IOSIF Radu, KONEČNÝ Filip and VOJNAR Tomáš. Automatic Verification of Integer Array Programs. In: Computer Aided Verification. Lecture Notes in Computer Science, vol. 5643. Berlin: Springer Verlag, 2009, pp. 157-172. ISBN 978-3-642-02657-7.
Czech title
Automatická verifikace programů s poli
Type
conference paper
Language
english
Authors
Bozga Marius (VERIMAG)
Habermehl Peter (UPAR7)
Iosif Radu (VERIMAG)
Konečný Filip, Ing. (DITS FIT BUT)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
URL
Keywords

formal verification, arrays, automata, mathematical logic

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}.
Published
2009
Pages
157-172
Proceedings
Computer Aided Verification
Series
Lecture Notes in Computer Science
Volume
5643
Conference
21st International Conference on Computer Aided Verification -- CAV 2009, Grenoble, FR
ISBN
978-3-642-02657-7
Publisher
Springer Verlag
Place
Berlin, DE
BibTeX 
@INPROCEEDINGS{FITPUB9005,
   author = "Marius Bozga and Peter Habermehl and Radu Iosif and Filip Kone\v{c}n\'{y} and Tom\'{a}\v{s} Vojnar",
   title = "Automatic Verification of Integer Array Programs",
   pages = "157--172",
   booktitle = "Computer Aided Verification",
   series = "Lecture Notes in Computer Science",
   volume = 5643,
   year = 2009,
   location = "Berlin, DE",
   publisher = "Springer Verlag",
   ISBN = "978-3-642-02657-7",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/9005"
}
Back to top