| Identifikační kód | RIV/00216224:14330/11:00052855 |
|---|
| Název v anglickém jazyce | Efficient Loop Navigation for Symbolic Execution |
|---|
| Druh | D - Článek ve sborníku |
|---|
| Jazyk | eng - angličtina |
|---|
| Obor - skupina | I - Informatika |
|---|
| Obor | IN - Informatika |
|---|
| Rok uplatnění | 2011 |
|---|
| Kód důvěrnosti údajů | S - Úplné a pravdivé údaje o výsledku nepodléhající ochraně podle zvláštních právních předpisů. |
|---|
| Počet výskytů výsledku | 1 |
|---|
| Počet tvůrců celkem | 2 |
|---|
| Počet domácích tvůrců | 2 |
|---|
| Výčet všech uvedených jednotlivých tvůrců | Jan Obdržálek (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 3294099)
Marek Trtík (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 9937056) |
|---|
| Popis výsledku v anglické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 targetlocation 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. Onreaching 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 oddělená středníkem | symbolic execution; loops in programs; program verification; bug-finding |
|---|
| Stránka www, na které se nachází výsledek | - |
|---|
| DOI výsledku | 10.1007/978-3-642-24372-1_34 |
|---|