Symbolic Memory with Pointers
| Authors | |
|---|---|
| Year of publication | 2014 |
| Type | Article in Proceedings |
| Conference | Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014 |
| MU Faculty or unit | |
| 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: |