Anzeige
Erschienen in:
2009 | OriginalPaper | Buchkapitel
Automatic Verification of Integer Array Programs
verfasst von : Marius Bozga, Peter Habermehl, Radu Iosif, Filip Konečný, Tomáš Vojnar
Erschienen in: Computer Aided Verification
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
We provide a verification technique for a class of programs working on
integer arrays
of finite, but not a priori bounded length. We use the logic of integer arrays
SIL
[13] 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
SIL
. Loop pre-conditions derived during the computation in
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
SIL
formulae, thus inferring post-conditions of the loops. Finally, validity of post-conditions specified by the user in
SIL
may be checked as entailment is decidable for
SIL
.