Symbolic Memory with Pointers

TRTÍK, Marek a Jan STREJČEK. Symbolic Memory with Pointers. In Franck Cassez and Jean-Francois Raskin. Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014. Berlin Heidelberg: Springer, 2014, s. 380-395. ISBN 978-3-319-11935-9. Dostupné z: https://dx.doi.org/10.1007/978-3-319-11936-6_27.

Základní údaje

• Originální název: Symbolic Memory with Pointers
• Název česky: Symbolická paměť s ukazateli
• Autoři: TRTÍK, Marek (203 Česká republika, domácí) a Jan STREJČEK (203 Česká republika, garant, domácí).
• Vydání: Berlin Heidelberg, Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014, od s. 380-395, 16 s. 2014.
• Nakladatel: Springer

Další údaje

• Originální jazyk: angličtina
• Typ výsledku: Stať ve sborníku
• Obor: 10201 Computer sciences, information science, bioinformatics
• Stát vydavatele: Německo
• Utajení: není předmětem státního či obchodního tajemství
• Forma vydání: tištěná verze "print"
• Impakt faktor: Impact factor: 0.402 v roce 2005
• Kód RIV: RIV/00216224:14330/14:00074092
• Organizační jednotka: Fakulta informatiky
• ISBN: 978-3-319-11935-9
• ISSN: 0302-9743
• Doi: http://dx.doi.org/10.1007/978-3-319-11936-6_27
• Klíčová slova anglicky: symbolic execution; symbolic memory
• Štítky: core_A, firank_A, formela-conference
• Příznaky: Mezinárodní význam, Recenzováno

Anotace

We introduce a segment-offset-plane memory model for symbolic execution that supports symbolic pointers, allocations of memory blocks of symbolic sizes, and multi-writes. We further describe our efficient implementation of the model in a free open-source project Bugst. Experimental results provide empirical evidence that the implemented memory model effectively tackles the variable storage-referencing problem of symbolic execution.

Anotace česky

Představujeme paměťový model pro symbolickou exekuci nazvaný "segment-offset-plane", který podporuje symbolické ukazatele, alokaci paměti symbolické velikosti, a současný zápis do více paměťových míst. Dále popisujeme naši efektivní implementaci tohoto modelu ve volně šiřitelném open-source projektu Bugst. Experimentální výsledky ukazují, že naše implementace zmíněného modelu paměti efektivně potlačuje problém symbolické exekuce s proměnnými (tj. ne konkrétními) odkazy do paměti.

Návaznosti

• GBP202/12/G061, projekt VaV: Název: Centrum excelence - Institut teoretické informatiky (CE-ITI) (Akronym: CE-ITI)

Investor: Grantová agentura ČR, Centrum excelence - Institut teoretické informatiky

• MUNI/A/0765/2013, interní kód MU: Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Akronym: SKOMU)

Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

• MUNI/A/0855/2013, interní kód MU: Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace III. (Akronym: FI MAV III.)

Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace III., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty