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. |
Další formáty:
BibTeX
LaTeX
RIS
|
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 |
Změnil | Změnil: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Změněno: 13. 11. 2014 16:23. |
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 |
VytisknoutZobrazeno: 10. 10. 2024 07:14