zbMATH — the first resource for mathematics

Symbolic memory with pointers. (English) Zbl 1448.68222
Cassez, Franck (ed.) et al., Automated technology for verification and analysis. 12th international symposium, ATVA 2014, Sydney, NSW, Australia, November 3–7, 2014. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 8837, 380-395 (2014).
Summary: 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.
For the entire collection see [Zbl 1325.68014].
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Bugst; CUTE; KLEE; Pex; z3
Full Text: DOI