We propose a new approach to shape analysis of programs with linked lists that use low-level memory operations. Such operations include pointer arithmetic, safe usage of invalid pointers, block operations with memory, reinterpretation of the memory contents, address alignment, etc. Our approach is based on a new representation of sets of heaps, which is to some degree inspired by works on separation logic with higher-order list predicates, but it is graph-based and uses a more fine-grained (byte-precise) memory model in order to support the various low-level memory operations. The approach was implemented in the Predator tool and successfully validated on multiple non-trivial case studies that are beyond the capabilities of other current fully automated shape analysis tools. © 2013 Springer-Verlag.
CITATION STYLE
Dudka, K., Peringer, P., & Vojnar, T. (2013). Byte-precise verification of low-level list manipulation. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7935 LNCS, pp. 215–237). https://doi.org/10.1007/978-3-642-38856-9_13
Mendeley helps you to discover research relevant for your work.