Symbolic Memory with Pointers

TRTÍK, Marek and 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, p. 380-395. ISBN 978-3-319-11935-9. Available from: https://dx.doi.org/10.1007/978-3-319-11936-6_27.

Basic information

Original name

Symbolic Memory with Pointers

Name in Czech

Symbolická paměť s ukazateli

Authors

TRTÍK, Marek (203 Czech Republic, belonging to the institution) and Jan STREJČEK (203 Czech Republic, guarantor, belonging to the institution)

Edition

Berlin Heidelberg, Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014, p. 380-395, 16 pp. 2014

Publisher

Springer

---

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Germany

Confidentiality degree

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

Publication form

printed version "print"

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/14:00074092

Organization unit

Faculty of Informatics

ISBN

978-3-319-11935-9

ISSN

DOI

http://dx.doi.org/10.1007/978-3-319-11936-6_27

Keywords in English

symbolic execution; symbolic memory

Tags

core_A, firank_A, formela-conference

Tags

International impact, Reviewed

---

Abstract

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.

In Czech

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.

---

Links

GBP202/12/G061, research and development project	Name: Centrum excelence - Institut teoretické informatiky (CE-ITI) (Acronym: CE-ITI) Investor: Czech Science Foundation
MUNI/A/0765/2013, interní kód MU	Name: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Acronym: SKOMU) Investor: Masaryk University, Category A
MUNI/A/0855/2013, interní kód MU	Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace III. (Acronym: FI MAV III.) Investor: Masaryk University, Category A