Publication Details

Automatic Verification of Integer Array Programs

IOSIF, R.; KONEČNÝ, F.; VOJNAR, T.; HABERMEHL, P.; BOZGA, M. Automatic Verification of Integer Array Programs. Computer Aided Verification. Lecture Notes in Computer Science. Berlin: Springer Verlag, 2009. p. 157-172. ISBN: 978-3-642-02657-7.
Czech title
Automatická verifikace programů s poli
Type
conference paper
Language
English
Authors
Radu Iosif
Konečný Filip, Ing., Ph.D.
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)
Habermehl Peter
Bozga Marius
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
ISBN
978-3-642-02657-7
Publisher
Springer Verlag
Place
Berlin
BibTeX 
@inproceedings{BUT30759,
  author="Iosif {Radu} and Filip {Konečný} and Tomáš {Vojnar} and Peter {Habermehl} and Marius {Bozga}",
  title="Automatic Verification of Integer Array Programs",
  booktitle="Computer Aided Verification",
  year="2009",
  series="Lecture Notes in Computer Science",
  volume="5643",
  pages="157--172",
  publisher="Springer Verlag",
  address="Berlin",
  isbn="978-3-642-02657-7",
  url="https://www.fit.vut.cz/research/publication/9005/"
}
Back to top