Článek ve sborníku konference

 
Bozga, M., Habermehl, P., Iosif, R., Konečný, F., Vojnar, T.: Automatic Verification of Integer Array Programs, In: Computer Aided Verification, Berlin, DE, Springer, 2009, s. 157-172, ISBN 978-3-642-02657-7
Jazyk publikace:angličtina
Název publikace:Automatic Verification of Integer Array Programs
Název (cs):Automatická verifikace programů s poli
Strany:157-172
Sborník:Computer Aided Verification
Konference:21st International Conference on Computer Aided Verification -- CAV 2009
Řada knih:Lecture Notes in Computer Science 5643
Místo vydání:Berlin, DE
Rok:2009
ISBN:978-3-642-02657-7
Vydavatel:Springer Verlag
URL:http://www.fit.vutbr.cz/~ikonecny/pubs/CAV09.pdf [PDF]
URL:http://www.fit.vutbr.cz/~ikonecny/pubs/CAV09.ps [PS]
Klíčová slova
formální verifikace, pole, automaty, matematická logika
Anotace
Č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:
@INPROCEEDINGS{
   author = {Marius Bozga and Peter Habermehl and Radu Iosif and Filip
	Konečný and Tomáš Vojnar},
   title = {Automatic Verification of Integer Array Programs},
   pages = {157--172},
   booktitle = {Computer Aided Verification},
   series = {Lecture Notes in Computer Science 5643},
   year = {2009},
   location = {Berlin, DE},
   publisher = {Springer Verlag},
   ISBN = {978-3-642-02657-7},
   language = {english},
   url = {http://www.fit.vutbr.cz/research/view_pub.php?id=9005}
}