Detail publikace

Automatic Verification of Integer Array Programs

BOZGA Marius, HABERMEHL Peter, IOSIF Radu, KONEČNÝ Filip a VOJNAR Tomáš. Automatic Verification of Integer Array Programs. In: Computer Aided Verification. Lecture Notes in Computer Science, roč. 5643. Berlin: Springer Verlag, 2009, s. 157-172. ISBN 978-3-642-02657-7.
Název česky
Automatická verifikace programů s poli
Typ
článek ve sborníku konference
Jazyk
angličtina
Autoři
Bozga Marius (VERIMAG)
Habermehl Peter (UPAR7)
Iosif Radu (VERIMAG)
Konečný Filip, Ing. (UITS FIT VUT)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT)
URL
Klíčová slova

formální verifikace, pole, automaty, matematická logika

Abstrakt

Článek představuje verifikační metodu pro třídu programů, které manipulují s poli konečné, ale nikoliv předem omezené délky. Pro specifikaci vstupních a výstupních podmínek programu a jeho částí používáme logiku celočíselných polí (SIL). Účinky částí kódu bez cyklů jsou vypočítány syntakticky na úrovni logiky SIL. Takto odvozené vstupní podnínky cyklu jsou transformovány na čítačové automaty (CA). Cykly jsou automaticky, čistě na syntaktické úrovni, přeloženy do čítačových převodníků. Automaty reprezentující vstupní podmínky jsou složeny s převodníky a takto vzniklé automaty nadaproximovány 'flat'  čítačovým automatem s diferenčními omezeními a ten je dále převeden na odpovídající SIL formuli. Tímto obdržíme výstupní podmínku cyklu. Platnost uživatelem specifikované výstupní podmínky lze ověřit, neboť logika SIL je rozhodnutelná.

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, Grenoble, FR
ISBN
978-3-642-02657-7
Vydavatel
Springer Verlag
Místo
Berlin, DE
BibTeX
@INPROCEEDINGS{FITPUB9005,
   author = "Marius Bozga and Peter Habermehl and Radu Iosif and Filip Kone\v{c}n\'{y} and Tom\'{a}\v{s} Vojnar",
   title = "Automatic Verification of Integer Array Programs",
   pages = "157--172",
   booktitle = "Computer Aided Verification",
   series = "Lecture Notes in Computer Science",
   volume = 5643,
   year = 2009,
   location = "Berlin, DE",
   publisher = "Springer Verlag",
   ISBN = "978-3-642-02657-7",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/9005"
}
Nahoru