Publication Details

Byte-Precise Verification of Low-Level List Manipulation

DUDKA, K.; PERINGER, P.; VOJNAR, T. 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
report
Language
English
Authors
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
BibTeX
@techreport{BUT192900,
  author="Kamil {Dudka} and Petr {Peringer} and Tomáš {Vojnar}",
  title="Byte-Precise Verification of Low-Level List Manipulation",
  year="2013",
  publisher="Faculty of Information Technology BUT",
  address="FIT-TR-2012-04, Brno",
  pages="48",
  url="http://www.fit.vutbr.cz/research/groups/verifit/tools/predator/FIT-TR-2012-04.pdf"
}
Back to top