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. 157172. ISBN 9783642026577.  Publication language:  english 

Original title:  Automatic Verification of Integer Array Programs 

Title (cs):  Automatická verifikace programů s poli 

Pages:  157172 

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:  9783642026577 

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 postconditions of programs and their parts. Effects of nonlooping parts of code are computed
syntactically on the level of \textbf{SIL}. Loop preconditions derived during the computation in \textbf{SIL} are
converted into counter automata (CA). Loops are automatically translatedpurely on the syntactical levelto
transducers. Precondition CA and transducers are composed, and the composition overapproximated by flat automata with
difference bound constraints, which are next converted back into \textbf{SIL} formulae, thus inferring postconditions
of the loops. Finally, validity of postconditions 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čný and Tomáš Vojnar},
title = {Automatic Verification of Integer Array Programs},
pages = {157172},
booktitle = {Computer Aided Verification},
series = {Lecture Notes in Computer Science 5643},
year = {2009},
location = {Berlin, DE},
publisher = {Springer Verlag},
ISBN = {9783642026577},
language = {english},
url = {http://www.fit.vutbr.cz/research/view_pub.php?id=9005}
} 
