Efficient Loop Navigation for Symbolic Execution
The result's identifiers
Result code in 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>
Result on the web
<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>
Alternative languages
Result language
angličtina
Original language name
Efficient Loop Navigation for Symbolic Execution
Original language description
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.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
IN - Informatics
OECD FORD branch
—
Result continuities
Project
<a href="/en/project/1M0545" target="_blank" >1M0545: Institute for Theoretical Computer Science</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach
Others
Publication year
2011
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Automated Technology for Verification and Analysis, 9th International Symposium, ATVA 2011
ISBN
978-3-642-24371-4
ISSN
—
e-ISSN
—
Number of pages
10
Pages from-to
453-462
Publisher name
Springer-Verlag
Place of publication
Heidelberg
Event location
Taipei, Taiwan
Event date
Jan 1, 2011
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—