OBDRŽÁLEK, Jan a 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, s. 453-462. ISBN 978-3-642-24371-4. Dostupné z: https://dx.doi.org/10.1007/978-3-642-24372-1_34.
Další formáty:   BibTeX LaTeX RIS
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
Originální 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 http://dx.doi.org/10.1007/978-3-642-24372-1_34
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ěnil Změnil: doc. Mgr. Jan Obdržálek, PhD., učo 1552. Změněno: 16. 4. 2012 11:02.
Anotace
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 MUNá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 MUNá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 VaVNázev: Institut Teoretické Informatiky
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky
VytisknoutZobrazeno: 27. 9. 2024 05:28