Conference paperBOZGA Marius, HABERMEHL Peter, IOSIF Radu, KONEČNÝ Filip and VOJNAR Tomáš. Automatic Verification of Integer Array Programs. In: Computer Aided Verification. Berlin: Springer Verlag, 2009, pp. 157-172. ISBN 978-3-642-02657-7. | Publication language: | english |
---|
Original title: | Automatic Verification of Integer Array Programs |
---|
Title (cs): | Automatická verifikace programů s poli |
---|
Pages: | 157-172 |
---|
Proceedings: | Computer Aided Verification |
---|
Conference: | 21st International Conference on Computer Aided Verification -- CAV 2009 |
---|
Series: | Lecture Notes in Computer Science 5643 |
---|
Place: | Berlin, DE |
---|
Year: | 2009 |
---|
ISBN: | 978-3-642-02657-7 |
---|
Publisher: | Springer Verlag |
---|
URL: | http://www.fit.vutbr.cz/~ikonecny/pubs/CAV09.pdf [PDF] |
---|
URL: | http://www.fit.vutbr.cz/~ikonecny/pubs/CAV09.ps [PS] |
---|
Keywords |
---|
formal verification, arrays, automata, mathematical logic |
Annotation |
---|
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{
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 5643},
year = {2009},
location = {Berlin, DE},
publisher = {Springer Verlag},
ISBN = {978-3-642-02657-7},
language = {english},
url = {http://www.fit.vutbr.cz/research/view_pub.php?id=9005}
} |
|