Informace o publikaci

Compact Symbolic Execution

Název česky Kompaktní symbolická exekuce
Autoři

SLABÝ Jiří STREJČEK Jan TRTÍK Marek

Druh Článek ve sborníku
Konference 11th International Symposium on Automated Technology for Verification and Analysis, ATVA 2013
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
Doi http://dx.doi.org/10.1007/978-3-319-02444-8_15
Obor Informatika
Klíčová slova symbolic execution; compact symbolic execution; testing
Popis Prezentujeme zobecnění Kingovy symbolické exekuce nazvané kompaktní symbolická exekuce. Tato zobecněná technika pracuje ve dvou krocích. Nejdříve se analyzují cyklické cesty v grafu toku řízení daného programu nezávisle na zbytku programu. Cílem této analýzy je nalézt pro každou cyklickou cestu takzvanou šablonu. Šablona je deklarativní parametrický popis všech možných programových stavů, kterými lze opustit analyzovanou cyklickou cestu po nějakém počtu iterací podél této cesty. V druhém kroku spouštíme program symbolicky s využitím těchto šablon. Výsledkem je strom kompaktní symbolické exekuce. Tento strom nese v listech stejnou informaci jako odpovídající strom klasické symbolické exekuce. Ovšem kompaktní strom je obvykle podstatně menší než odpovídající klasický strom. Existují programy, pro které je kompaktní strom konečný, zatímco klasický strom je nekonečný.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.

Další info