SLABÝ, Jiří, Jan STREJČEK a Marek TRTÍK. Compact Symbolic Execution. In Hung Dang-Van and Mizuhito Ogawa. 11th International Symposium on Automated Technology for Verification and Analysis, ATVA 2013. Berlin Heidelberg: Springer. s. 193-207. ISBN 978-3-319-02443-1. doi:10.1007/978-3-319-02444-8_15. 2013.
Další formáty:   BibTeX LaTeX RIS
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
Originální 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 0302-9743
Doi http://dx.doi.org/10.1007/978-3-319-02444-8_15
Klíčová slova anglicky symbolic execution; compact symbolic execution; testing
Štítky core_A, firank_A, formela-conference
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Změněno: 18. 11. 2013 14:45.
Anotace
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.
Anotace č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 VaVNá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 MUNá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 MUNá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
VytisknoutZobrazeno: 16. 4. 2024 13:25