Conference paper

DUDKA Kamil, PERINGER Petr and VOJNAR Tomáš. Byte-Precise Verification of Low-Level List Manipulation. In: 20th Static Analysis Symposium. Berlin: Springer Verlag, 2013, pp. 215-237. ISBN 978-3-642-38855-2. ISSN 0302-9743.
Publication language:english
Original title:Byte-Precise Verification of Low-Level List Manipulation
Title (cs):Nízkoúrovňová verifikace manipulace seznamů
Proceedings:20th Static Analysis Symposium
Conference:20th International Static Analysis Symposium -- SAS 2013
Series:Lecture Notes in Computer Science Volume 7935
Place:Berlin, DE
Journal:Lecture Notes in Computer Science, Vol. 20, No. 7935, DE
Publisher:Springer Verlag
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
   pages = {215--237},
   booktitle = {20th Static Analysis Symposium},
   series = {Lecture Notes in Computer Science Volume 7935},
   journal = {Lecture Notes in Computer Science},
   volume = 20,
 number = 7935,
   year = 2013,
   location = {Berlin, DE},
   publisher = {Springer Verlag},
   ISBN = {978-3-642-38855-2},
   ISSN = {0302-9743},
   language = {english},
   url = {}

Your IPv4 address:
Switch to https