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

článek ve sborníku mimo WoS a Scopus

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.

Rok RIV

2013

Vydáno

12. 5. 2013

Nakladatel

Springer Verlag

Místo

Berlin

ISBN

978-3-642-38855-2

Kniha

20th Static Analysis Symposium

Edice

Lecture Notes in Computer Science Volume 7935

ISSN

0302-9743

Periodikum

Lecture Notes in Computer Science

Ročník

20

Číslo

7935

Stát

Spolková republika Německo

Strany od

215

Strany do

237

Strany počet

23

BibTex

@inproceedings{BUT103494,
  author="Kamil {Dudka} and Petr {Peringer} and Tomáš {Vojnar}",
  title="Byte-Precise Verification of Low-Level List Manipulation",
  booktitle="20th Static Analysis Symposium",
  year="2013",
  series="Lecture Notes in Computer Science Volume 7935",
  journal="Lecture Notes in Computer Science",
  volume="20",
  number="7935",
  pages="215--237",
  publisher="Springer Verlag",
  address="Berlin",
  isbn="978-3-642-38855-2",
  issn="0302-9743"
}