Compact Symbolic Execution

• Název česky: Kompaktní symbolická exekuce
• Autoři: SLABÝ Jiří; STREJČEK Jan; TRTÍK Marek
• Rok publikování: 2013
• 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
• 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

• Centrum excelence - Institut teoretické informatiky
• Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity
• Rozsáhlé výpočetní systémy: modely, aplikace a verifikace II.