| Údaje o výsledku |
| Identifikační kód | RIV/00216224:14330/11:00052855 |
| Název v původním jazyce | Efficient Loop Navigation for Symbolic Execution |
| Druh | D - Článek ve sborníku |
| Jazyk | eng - angličtina |
| Obor | IN - Informatika |
| Rok uplatnění | 2011 |
| 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 | 1 |
| Ú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 | Výsledek hodnocený již v předchozím hodnocení, body se přebírají |
| Bodové ohodnocení | 44,387 |
| Faktor korekce | 100,9 % |
| Body (upravené podle přílohy č. 8 Metodiky) | 44,799 |
| 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 % | 44,387 | 44,799 |
|
| Tvůrci výsledku |
| Počet tvůrců celkem | 2 |
| Počet domácích tvůrců | 2 |
| Tvůrce | Obdržálek Jan (státní příslušnost: CZ - Česká republika; A - domácí tvůrce; G - garant výsledku; vedidk: 3294099) |
| 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 | Symbolic execution is a successful technique used in software verification and testing. A key limitation of symbolic execution is in dealing with code containing loops. We introduce a technique which, given a start location above some loops and a target location anywhere below these loops, returns a feasible path between these two locations, if such a path exists. The technique infers a collection of constraint systems from the program and uses them to steer the symbolic execution towards the target. On reaching a loop it iteratively solves the appropriate constraint system to find out which path through this loop to take, or, alternatively, whether to continue below the loop. To construct the constraint systems we express the values of variables modified in a loop as functions of the number of times a given path through the loop was executed. |
| Klíčová slova | symbolic execution; loops in programs; program verification; bug-finding |
| Rozsah stran | 453-462 |
| Název sborníku | Automated Technology for Verification and Analysis, 9th International Symposium, ATVA 2011 |
| Počet stran výsledku | 10 |
| ISBN | 978-3-642-24371-4 |
| Název nakladatele | Springer-Verlag |
| Místo vydání | Heidelberg |
| Místo konání akce | Taipei, Taiwan |
| Rok konání akce | 2011 |
| Typ akce podle státní příslušnoti účastníků | WRD - Světová |
| DOI výsledku | 10.1007/978-3-642-24372-1_34 |
| Ú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 | 2012 |
| Systémové označení dodávky dat | RIV12-MSM-14330___/01:1 |
| Specifikace | RIV/00216224:14330/11:00052855!RIV12-MSM-14330___ |
| Kontrolní kód | [0E140B3BDB94] |
| Jiný výskyt tohoto výsledku se v RIV nenachází |
| Odkazy na výzkumné aktivity, při jejichž řešení výsledek vznikl |
| Projekt | 1M0545 - Institut Teoretické Informatiky (2005-2011, MSM/1M) |
| S - Specifický výzkum na vysokých školách |