Technical report

DUDKA Kamil, PERINGER Petr and VOJNAR Tomáš. Byte-Precise Verification of Low-Level List Manipulation. FIT-TR-2012-04, Brno: Faculty of Information Technology BUT, 2013.
Publication language:english
Original title:Byte-Precise Verification of Low-Level List Manipulation
Title (cs):Nízkoúrovňová verifikace manipulace seznamů
Place:FIT-TR-2012-04, Brno, CZ
Publisher:Faculty of Information Technology BUT
dynamic linked data structures
separation logic
symbolic memory graphs
list manipulation
low-level memory manipulation
memory safety
shape analysis
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.
   author = {Kamil Dudka and Petr Peringer and Tom{\'{a}}{\v{s}} Vojnar},
   title = {Byte-Precise Verification of Low-Level List Manipulation},
   pages = {48},
   year = {2013},
   location = {FIT-TR-2012-04, Brno, CZ},
   publisher = {Faculty of Information Technology BUT},
   language = {english},
   url = {}

Your IPv4 address:
Switch to IPv6 connection

DNSSEC [dnssec]