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

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

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

V originále

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.

Č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