Symbolic Memory with Pointers

Investor logo

Warning

This publication doesn't include Faculty of Education. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

TRTÍK Marek STREJČEK Jan

Year of publication 2014
Type Article in Proceedings
Conference Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014
MU Faculty or unit

Faculty of Informatics

Citation
Doi http://dx.doi.org/10.1007/978-3-319-11936-6_27
Field Informatics
Keywords symbolic execution; symbolic memory
Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.