Detail výsledku

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.
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Radu Iosif
Konečný Filip, Ing., Ph.D., UITS (FIT)
Vojnar Tomáš, prof. Ing., Ph.D., UITS (FIT)
Habermehl Peter
Bozga Marius
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

URL
Rok
2009
Strany
157–172
Sborník
Computer Aided Verification
Řada
Lecture Notes in Computer Science
Svazek
5643
Konference
21st International Conference on Computer Aided Verification -- CAV 2009
ISBN
978-3-642-02657-7
Vydavatel
Springer Verlag
Místo
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/"
}
Projekty
Matematické a inženýrské metody pro vývoj spolehlivých a bezpečných paralelních a distribuovaných počítačových systémů, GAČR, Doktorské granty, GD102/09/H042, zahájení: 2009-01-30, ukončení: 2012-12-31, ukončen
Pokročilé formální přístupy v návrhu a automatické verifikaci počítačových systémů, GAČR, Standardní projekty, GA102/07/0322, zahájení: 2007-01-01, ukončení: 2009-12-31, ukončen
Výzkum informačních technologií z hlediska bezpečnosti, MŠMT, Institucionální prostředky SR ČR (např. VZ, VC), MSM0021630528, zahájení: 2007-01-01, ukončení: 2013-12-31, řešení
Výzkumné skupiny
Výzkumná skupina automatizované analýzy a verifikace - VeriFIT (VZ VERIFIT)
Pracoviště
Ústav inteligentních systémů (UITS)
Nahoru