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. p. 0-0.
Czech title
Nízkoúrovňová verifikace manipulace seznamů
Type
report
Language
English
Authors
Dudka Kamil, Ing.
Peringer Petr, Dr. Ing. (DITS)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)
URL
Keywords

dynamic linked data structuresseparation logic
symbolic memory graphslist manipulationlow-level memory manipulationmemory
safetyshape 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