Technická zprávaBOZGA Marius, HABERMEHL Peter, IOSIF Radu, KONEČNÝ Filip a VOJNAR Tomáš. Automatic Verification of Integer Array Programs. TR-2009-2, Grenoble: VERIMAG, 2009. | Jazyk publikace: | angličtina |
---|
Název publikace: | Automatic Verification of Integer Array Programs |
---|
Název (cs): | Automatická verifikace programů s poli |
---|
Strany: | 49 |
---|
Místo vydání: | TR-2009-2, Grenoble, FR |
---|
Rok: | 2009 |
---|
Vydavatel: | VERIMAG |
---|
URL: | http://www-verimag.imag.fr/TR/TR-2009-2.pdf [PDF] |
---|
Klíčová slova |
---|
formální verifikace, pole, automaty, matematická logika |
Anotace |
---|
Jedná se úplnou verzi článku publikovaného na CAV'09. Č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á.
|
BibTeX: |
---|
@TECHREPORT{
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 = {49},
year = {2009},
location = {TR-2009-2, Grenoble, FR},
publisher = {VERIMAG},
language = {english},
url = {http://www.fit.vutbr.cz/research/view_pub.php.cs?id=9006}
} |
|