Conference paper

 
Bozga, M., Habermehl, P., Iosif, R., Konečný, F., Vojnar, T.: Automatic Verification of Integer Array Programs, In: Computer Aided Verification, Berlin, DE, Springer, 2009, p. 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čný and Tomáš 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}
}