Detail publikačního výsledku

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

Anglický název

Automatic Verification of Integer Array Programs

Druh

Stať ve sborníku mimo WoS a Scopus

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

Anglický 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

Klíčová slova v angličtině

formal verification, arrays, automata, mathematical logic

Autoři

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

Rok RIV

2010

Vydáno

23.06.2009

Nakladatel

Springer Verlag

Místo

Berlin

ISBN

978-3-642-02657-7

Kniha

Computer Aided Verification

Edice

Lecture Notes in Computer Science

Svazek

5643

Strany od

157

Strany do

172

Strany počet

16

URL

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

Plný text v Digitální knihovně

http://hdl.handle.net/

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