Publication Details

Byte-Precise Verification of Low-Level List Manipulation

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.
Czech title
Nízkoúrovňová verifikace manipulace seznamů
Type
technical report
Language
english
Authors
Dudka Kamil, Ing. (DITS FIT BUT)
Peringer Petr, Dr. Ing. (DITS FIT BUT)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
URL
Keywords
dynamic linked data structures
separation logic
symbolic memory graphs
list manipulation
low-level memory manipulation
memory safety
shape analysis
Abstract

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.

Published
2013
Pages
48
Publisher
Faculty of Information Technology BUT
Place
FIT-TR-2012-04, Brno, CZ
BibTeX
@TECHREPORT{FITPUB10330,
   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 = "https://www.fit.vut.cz/research/publication/10330"
}
Back to top