Detail publikace

Automatic Verification of Integer Array Programs

IOSIF, R. KONEČNÝ, F. VOJNAR, T. HABERMEHL, P. BOZGA, M.

Originální název

Automatic Verification of Integer Array Programs

Typ

článek ve sborníku mimo WoS a Scopus

Jazyk

angličtina

Originální abstrakt

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}.

Klíčová slova

formal verification, arrays, automata, mathematical logic

Autoři

IOSIF, R.; KONEČNÝ, F.; VOJNAR, T.; HABERMEHL, P.; BOZGA, M.

Rok RIV

2009

Vydáno

23. 6. 2009

Nakladatel

Springer Verlag

Místo

Berlin

ISBN

978-3-642-02657-7

Kniha

Computer Aided Verification

Edice

Lecture Notes in Computer Science

Strany od

157

Strany do

172

Strany počet

16

URL

https://www.fit.vut.cz/research/publication/9005/

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/"
}