Faculty of Information Technology, BUT

Publication Details

Byte-Precise Verification of Low-Level List Manipulation

DUDKA Kamil, PERINGER Petr and VOJNAR Tomáš. Byte-Precise Verification of Low-Level List Manipulation. In: 20th Static Analysis Symposium. Lecture Notes in Computer Science Volume 7935, vol. 20. Berlin: Springer Verlag, 2013, pp. 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
Dudka Kamil, Ing. (DITS FIT BUT)
Peringer Petr, Dr. Ing. (DITS FIT BUT)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
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
Conference
20th International Static Analysis Symposium -- SAS 2013, Seattle, Washington, US
ISBN
978-3-642-38855-2
Publisher
Springer Verlag
Place
Berlin, DE
BibTeX
@INPROCEEDINGS{FITPUB10329,
   author = "Kamil Dudka and Petr Peringer and Tom\'{a}\v{s} Vojnar",
   title = "Byte-Precise Verification of Low-Level List Manipulation",
   pages = "215--237",
   booktitle = "20th Static Analysis Symposium",
   series = "Lecture Notes in Computer Science Volume 7935",
   journal = "Lecture Notes in Computer Science",
   volume = 20,
   number = 7935,
   year = 2013,
   location = "Berlin, DE",
   publisher = "Springer Verlag",
   ISBN = "978-3-642-38855-2",
   ISSN = "0302-9743",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/10329"
}
Back to top