Publication detail
Automatic Verification of Integer Array Programs
IOSIF, R. KONEČNÝ, F. VOJNAR, T. HABERMEHL, P. BOZGA, M.
Original Title
Automatic Verification of Integer Array Programs
Type
article in a collection out of WoS and Scopus
Language
English
Original 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}.
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}.
Keywords
formal verification, arrays, automata, mathematical logic
Authors
IOSIF, R.; KONEČNÝ, F.; VOJNAR, T.; HABERMEHL, P.; BOZGA, M.
RIV year
2009
Released
23. 6. 2009
Publisher
Springer Verlag
Location
Berlin
ISBN
978-3-642-02657-7
Book
Computer Aided Verification
Edition
Lecture Notes in Computer Science
Pages from
157
Pages to
172
Pages count
16
URL
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/"
}