Detail publikace

Automatic Verification of Integer Array Programs

IOSIF, R.; KONEČNÝ, F.; VOJNAR, T.; HABERMEHL, P.; BOZGA, M. Automatic Verification of Integer Array Programs. TR-2009-2, Grenoble: VERIMAG, 2009. p. 0-0.
Název česky
Automatická verifikace programů s poli
Typ
zpráva odborná
Jazyk
anglicky
Autoři
Radu Iosif
Konečný Filip, Ing., Ph.D.
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)
Habermehl Peter
Bozga Marius
URL
Klíčová slova

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

Abstrakt

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. Prospecifikaci 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 jsouslož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 naodpoví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
49
Vydavatel
VERIMAG
Místo
TR-2009-2, Grenoble
BibTeX 
@techreport{BUT192689,
  author="Iosif {Radu} and Filip {Konečný} and Tomáš {Vojnar} and Peter {Habermehl} and Marius {Bozga}",
  title="Automatic Verification of Integer Array Programs",
  year="2009",
  publisher="VERIMAG",
  address="TR-2009-2, Grenoble",
  pages="49",
  url="http://www-verimag.imag.fr/TR/TR-2009-2.pdf"
}
Nahoru