## Conference paper

Publication language: BOZGA, M., HABERMEHL, P., IOSIF, R., KONEČNÝ, F. and VOJNAR, T.. Automatic Verification of Integer Array Programs. In: Computer Aided Verification. Berlin: Springer Verlag, 2009, pp. 157-172. ISBN 978-3-642-02657-7. english Automatic Verification of Integer Array Programs Automatická verifikace programů s poli 157-172 Computer Aided Verification 21st International Conference on Computer Aided Verification -- CAV 2009 Lecture Notes in Computer Science 5643 Berlin, DE 2009 978-3-642-02657-7 Springer Verlag http://www.fit.vutbr.cz/~ikonecny/pubs/CAV09.pdf [PDF] http://www.fit.vutbr.cz/~ikonecny/pubs/CAV09.ps [PS] formal verification, arrays, automata, mathematical logic 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}. @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.en?id=9005} }