Detail publikace

Byte-Precise Verification of Low-Level List Manipulation

DUDKA, K. PERINGER, P. VOJNAR, T.

Originální název

Byte-Precise Verification of Low-Level List Manipulation

Typ

zpráva odborná

Jazyk

angličtina

Originální abstrakt

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.

Klíčová slova

dynamic linked data structures
separation logic
symbolic memory graphs
list manipulation
low-level memory manipulation
memory safety
shape analysis

Autoři

DUDKA, K.; PERINGER, P.; VOJNAR, T.

Vydáno

8. 4. 2013

Nakladatel

Faculty of Information Technology BUT

Místo

FIT-TR-2012-04, Brno

Strany počet

48

URL

http://www.fit.vutbr.cz/research/groups/verifit/tools/predator/FIT-TR-2012-04.pdf

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"
}