Efficient Loop Navigation for Symbolic Execution

D 2011

Efficient Loop Navigation for Symbolic Execution

OBDRŽÁLEK, Jan and Marek TRTÍK

Basic information

Original name

Efficient Loop Navigation for Symbolic Execution

Authors

OBDRŽÁLEK, Jan (203 Czech Republic, guarantor, belonging to the institution) and Marek TRTÍK (203 Czech Republic, belonging to the institution)

Edition

Heidelberg, Automated Technology for Verification and Analysis, 9th International Symposium, ATVA 2011, p. 453-462, 10 pp. 2011

Publisher

Springer-Verlag

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Czech Republic

Confidentiality degree

není předmětem státního či obchodního tajemství

RIV identification code

RIV/00216224:14330/11:00052855

Organization unit

Faculty of Informatics

ISBN

978-3-642-24371-4

DOI

http://dx.doi.org/10.1007/978-3-642-24372-1_34

UT WoS

000306498800034

Keywords in English

symbolic execution; loops in programs; program verification; bug-finding

Abstract

V originále

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.

Links

MUNI/A/0057/2011, interní kód MU

Name: Posílení zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Acronym: SKONF)

Investor: Masaryk University, Category A

MUNI/A/0914/2009, interní kód MU

Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace (Acronym: SV-FI MAV)

Investor: Masaryk University, Category A

1M0545, research and development project

Name: Institut Teoretické Informatiky

Investor: Ministry of Education, Youth and Sports of the CR, Institute for Theoretical Computer Science

Citovat

OBDRŽÁLEK, Jan and Marek TRTÍK. Efficient Loop Navigation for Symbolic Execution. In Tevfik Bultan and Pao-Ann Hsiung. Automated Technology for Verification and Analysis, 9th International Symposium, ATVA 2011. Heidelberg: Springer-Verlag, 2011, p. 453-462. ISBN 978-3-642-24371-4. Available from: https://dx.doi.org/10.1007/978-3-642-24372-1_34.

@inproceedings{947610,
   author = {Obdržálek, Jan and Trtík, Marek},
   address = {Heidelberg},
   booktitle = {Automated Technology for Verification and Analysis, 9th International Symposium, ATVA 2011},
   doi = {http://dx.doi.org/10.1007/978-3-642-24372-1_34},
   editor = {Tevfik Bultan and Pao-Ann Hsiung},
   keywords = {symbolic execution; loops in programs; program verification; bug-finding},
   language = {eng},
   location = {Heidelberg},
   isbn = {978-3-642-24371-4},
   pages = {453-462},
   publisher = {Springer-Verlag},
   title = {Efficient Loop Navigation for Symbolic Execution},
   year = {2011}
}

TY  - JOUR
ID  - 947610
AU  - Obdržálek, Jan - Trtík, Marek
PY  - 2011
TI  - Efficient Loop Navigation for Symbolic Execution
PB  - Springer-Verlag
CY  - Heidelberg
SN  - 9783642243714
KW  - symbolic execution
KW  - loops in programs
KW  - program verification
KW  - bug-finding
N2  - 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.
ER  -

OBDRŽÁLEK, Jan and Marek TRTÍK. Efficient Loop Navigation for Symbolic Execution. In Tevfik Bultan and Pao-Ann Hsiung. \textit{Automated Technology for Verification and Analysis, 9th International Symposium, ATVA 2011}. Heidelberg: Springer-Verlag, 2011, p.~453-462. ISBN~978-3-642-24371-4. Available from: https://dx.doi.org/10.1007/978-3-642-24372-1\_{}34.

Detailed Information on Publication Record