Verification of low-level C/C++ requires a precise memory model that supports type unions, pointer arithmetic, and casts. We present a new memory model that splits memory into a finite set of disjoint regions based on a pointer analysis. The main contribution is a field-, array- and context-sensitive pointer analysis tailored to verification. We have implemented our memory model for the LLVM bitcode and used it on a C++ case study and on SV-COMP benchmarks. Our results suggests that our model can reduce verification time by producing a finer-grained partitioning in presence of function calls.
CITATION STYLE
Gurfinkel, A., & Navas, J. A. (2017). A context-sensitive memory model for verification of C/C++ programs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10422 LNCS, pp. 148–168). Springer Verlag. https://doi.org/10.1007/978-3-319-66706-5_8
Mendeley helps you to discover research relevant for your work.