Symbolic Memory with Pointers

• 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
• 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

• Centrum excelence - Institut teoretické informatiky
• Rozsáhlé výpočetní systémy: modely, aplikace a verifikace III.
• Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity