Efficient Loop Navigation for Symbolic Execution

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F11%3A00052855" target="_blank" >RIV/00216224:14330/11:00052855 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1007/978-3-642-24372-1_34" target="_blank" >http://dx.doi.org/10.1007/978-3-642-24372-1_34</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-642-24372-1_34" target="_blank" >10.1007/978-3-642-24372-1_34</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Efficient Loop Navigation for Symbolic Execution

Popis výsledku 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 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.

Název v anglickém jazyce

Efficient Loop Navigation for Symbolic Execution

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

<a href="/cs/project/1M0545" target="_blank" >1M0545: Institut Teoretické Informatiky</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach

Rok uplatnění

2011

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Automated Technology for Verification and Analysis, 9th International Symposium, ATVA 2011

ISBN

978-3-642-24371-4

ISSN

—

e-ISSN

—

Počet stran výsledku

10

Strana od-do

453-462

Název nakladatele

Springer-Verlag

Místo vydání

Heidelberg

Místo konání akce

Taipei, Taiwan

Datum konání akce

1. 1. 2011

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—