| Údaje o výsledku |
| Identifikační kód | RIV/00216224:14330/13:00066165 |
| Název v původním jazyce | Compact Symbolic Execution |
| Druh | D - Článek ve sborníku |
| Jazyk | eng - angličtina |
| Obor | IN - Informatika |
| Rok uplatnění | 2013 |
| Kód důvěrnosti údajů | S - Úplné a pravdivé údaje nepodléhající ochraně podle zvláštních právních předpisů |
| Počet výskytů výsledku | 2 |
| Údaje z Hodnocení výsledků výzkumných organizací 2014 |
| Výsledek byl hodnocen v Pilíři I |
| Rozsah vyřazení výsledku | Tento výskyt výsledku není vyřazen |
| Zařazení výsledku v hodnocení | D - Článek ve sborníku |
| Skupina oboru v hodnocení | 04 - Technické a informatické vědy |
| Konkrétní způsob(y) hodnocení výsledku | Článek ve sborníku evidovaném v databázi Scopus bodovaný podle SJR zdroje typu Book Series nebo Conference Proceedings |
| Bodové ohodnocení | 46,181 |
| Faktor korekce | 50,1 % |
| Body (upravené podle přílohy č. 8 Metodiky) | 23,141 |
| Rozdělení výsledku mezi předkladatele |
| Organizace | Výzkumná organizace? | Podíl | Body | Body (upravené podle přílohy č. 8 Metodiky) |
|---|
| Masarykova univerzita / Fakulta informatiky | ano | 100,0 % | 46,181 | 23,141 |
|
| Tvůrci výsledku |
| Počet tvůrců celkem | 3 |
| Počet domácích tvůrců | 3 |
| Tvůrce | Slabý Jiří (státní příslušnost: CZ - Česká republika; A - domácí tvůrce; vedidk: 6545270) |
| Tvůrce | Strejček Jan (státní příslušnost: CZ - Česká republika; A - domácí tvůrce; vedidk: 3978915) |
| Tvůrce | Trtík Marek (státní příslušnost: CZ - Česká republika; A - domácí tvůrce; vedidk: 9937056) |
| Údaje blíže specifikující výsledek |
| Popis v původním jazyce | 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. |
| Klíčová slova | symbolic execution; compact symbolic execution; testing |
| Rozsah stran | 193-207 |
| Název sborníku | 11th International Symposium on Automated Technology for Verification and Analysis, ATVA 2013 |
| Forma vydání | P - Tištěná verze „print“ |
| ISSN | 0302-9743 |
| Počet stran výsledku | 15 |
| ISBN | 9783319024431 |
| Název nakladatele | Springer-Verlag |
| Místo vydání | Berlin Heidelberg |
| Místo konání akce | Hanoi, Vietnam |
| Rok konání akce | 2013 |
| Typ akce podle státní příslušnoti účastníků | WRD - Světová |
| DOI výsledku | 10.1007/978-3-319-02444-8_15 |
| Údaje o tomto záznamu o výsledku |
| Předkladatel | Masarykova univerzita / Fakulta informatiky |
| Dodavatel | MSM - Ministerstvo školství, mládeže a tělovýchovy (MŠMT) |
| Rok sběru | 2014 |
| Systémové označení dodávky dat | RIV14-MSM-14330___/01:1 |
| Specifikace | RIV/00216224:14330/13:00066165!RIV14-MSM-14330___ |
| Kontrolní kód | [B96DF5028FCD] |
| Další výskyty tohoto výsledku od stejného předkladatele |
| Dodáno GA ČR v roce 2014 | Záznam s identifikačním kódem RIV/00216224:14330/13:00066165 v dodávce dat RIV14-GA0-14330___/01:1 |
| Odkazy na výzkumné aktivity, při jejichž řešení výsledek vznikl |
| Projekt | GBP202/12/G061 - Centrum excelence - Institut teoretické informatiky (CE-ITI) (2012-2018, GA0/GB) |
| S - Specifický výzkum na vysokých školách |