D 2011

Efficient Loop Navigation for Symbolic Execution

OBDRŽÁLEK, Jan a Marek TRTÍK

Základní údaje

Originální název

Efficient Loop Navigation for Symbolic Execution

Autoři

OBDRŽÁLEK, Jan (203 Česká republika, garant, domácí) a Marek TRTÍK (203 Česká republika, domácí)

Vydání

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

Nakladatel

Springer-Verlag

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Česká republika

Utajení

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

Kód RIV

RIV/00216224:14330/11:00052855

Organizační jednotka

Fakulta informatiky

ISBN

978-3-642-24371-4

DOI

UT WoS

000306498800034

Klíčová slova anglicky

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

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 16. 4. 2012 11:02, doc. Mgr. Jan Obdržálek, PhD.

Anotace

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.

Návaznosti

MUNI/A/0057/2011, interní kód MU
Název: Posílení zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Akronym: SKONF)
Investor: Masarykova univerzita, Posílení zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
MUNI/A/0914/2009, interní kód MU
Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace (Akronym: SV-FI MAV)
Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
1M0545, projekt VaV
Název: Institut Teoretické Informatiky
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky