D 2013

Compact Symbolic Execution

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

Základní údaje

Originální název

Compact Symbolic Execution

Název česky

Kompaktní symbolická exekuce

Autoři

SLABÝ, Jiří (203 Česká republika, domácí), Jan STREJČEK (203 Česká republika, garant, domácí) a Marek TRTÍK (203 Česká republika, domácí)

Vydání

Berlin Heidelberg, 11th International Symposium on Automated Technology for Verification and Analysis, ATVA 2013, od s. 193-207, 15 s. 2013

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

tištěná verze "print"

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/13:00066165

Organizační jednotka

Fakulta informatiky

ISBN

978-3-319-02443-1

ISSN

DOI

Klíčová slova anglicky

symbolic execution; compact symbolic execution; testing

Štítky

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 18. 11. 2013 14:45, prof. RNDr. Jan Strejček, Ph.D.

Anotace

ORIG CZ

V originále

We present a generalisation of King’s symbolic execution technique called compact symbolic execution. It proceeds in two steps. First, we analyse cyclic paths in the control flow graph of a given program, independently from the rest of the program. Our goal is to compute a so called template for each such a cyclic path. A template is a declarative parametric description of all possible program states, which may leave the analysed cyclic path after any number of iterations along it. In the second step, we execute the program symbolically with the templates in hand. The result is a compact symbolic execution tree. A compact tree always carry the same information in all its leaves as the corresponding classic symbolic execution tree. Nevertheless, a compact tree is typically substantially smaller than the corresponding classic tree. There are even programs for which compact symbolic execution trees are finite while classic symbolic execution trees are infinite.

Česky

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ý.

Návaznosti

GBP202/12/G061, projekt VaV
Název: Centrum excelence - Institut teoretické informatiky (CE-ITI) (Akronym: CE-ITI)
Investor: Grantová agentura ČR, Centrum excelence - Institut teoretické informatiky
MUNI/A/0739/2012, interní kód MU
Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Akronym: SKOMU)
Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
MUNI/A/0760/2012, interní kód MU
Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace II. (Akronym: FI MAV II.)
Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace II., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty