Publication Details

Byte-Precise Verification of Low-Level List Manipulation

DUDKA, K.; PERINGER, P.; VOJNAR, T. Byte-Precise Verification of Low-Level List Manipulation. 20th Static Analysis Symposium. Lecture Notes in Computer Science. Lecture Notes in Computer Science Volume 7935. Berlin: Springer Verlag, 2013. p. 215-237. ISBN: 978-3-642-38855-2. ISSN: 0302-9743.
Czech title
Nízkoúrovňová verifikace manipulace seznamů
Type
conference paper
Language
English
Authors
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
215–237
Journal
Lecture Notes in Computer Science, vol. 20, no. 7935, ISSN 0302-9743
Proceedings
20th Static Analysis Symposium
Series
Lecture Notes in Computer Science Volume 7935
ISBN
978-3-642-38855-2
Publisher
Springer Verlag
Place
Berlin
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"
}
Back to top