Publication Details

From Low-Level Pointers to High-Level Containers

DUDKA Kamil, HOLÍK Lukáš, PERINGER Petr, TRTÍK Marek and VOJNAR Tomáš. From Low-Level Pointers to High-Level Containers. In: Verification, Model Checking, and Abstract Interpretation (VMCAI). Lecture Notes in Computer Science, vol. 9583. Berlin Heidelberg: Springer Verlag, 2016, pp. 431-452. ISBN 978-3-662-49121-8. Available from: http://www.springer.com/la/book/9783662491218
Czech title
Od nízkoúrovnňových ukazatelů k vysokoúrovňovým kontejnerům
Type
conference paper
Language
english
Authors
Dudka Kamil, Ing. (DITS FIT BUT)
Holík Lukáš, doc. Mgr., Ph.D. (DITS FIT BUT)
Peringer Petr, Dr. Ing. (DITS FIT BUT)
Trtík Marek, Mgr., Ph.D. (FI MUNI)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
URL
Keywords

program analysis, static analysis, shape analysis, heap abstraction, symbolic memory graphs, program transformation, pointer programs, container programs

Abstract

We propose a method that transforms a C program manipulating containers using low-level pointer statements into an equivalent program where the containers are manipulated via calls of standard high-level container operations like push_back or pop_front. The input of our method is a C program annotated by a special form of shape invariants which can be obtained from current automatic shape analysers after a slight modification. The resulting program where the low-level pointer statements are summarized into high-level container operations is more understandable and (among other possible benefits) better suitable for program analysis. We have implemented our approach and successfully tested it through a number of experiments with list-based containers, including experiments with simplification of program analysis by separating shape analysis from analysing data-related properties.

Published
2016
Pages
431-452
Proceedings
Verification, Model Checking, and Abstract Interpretation (VMCAI)
Series
Lecture Notes in Computer Science
Volume
9583
Conference
International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2016)/Symposium on Principles of Programming Languages (POPL 2016), St. Petersburg, Florida, US
ISBN
978-3-662-49121-8
Publisher
Springer Verlag
Place
Berlin Heidelberg, DE
DOI
10.1007/978-3-662-49122-5_21
UT WoS
000375148800021
EID Scopus
2-s2.0-84955248407
BibTeX 
@INPROCEEDINGS{FITPUB11060,
   author = "Kamil Dudka and Luk\'{a}\v{s} Hol\'{i}k and Petr Peringer and Marek Trt\'{i}k and Tom\'{a}\v{s} Vojnar",
   title = "From Low-Level Pointers to High-Level Containers",
   pages = "431--452",
   booktitle = "Verification, Model Checking, and Abstract Interpretation (VMCAI)",
   series = "Lecture Notes in Computer Science",
   volume = 9583,
   year = 2016,
   location = "Berlin Heidelberg, DE",
   publisher = "Springer Verlag",
   ISBN = "978-3-662-49121-8",
   doi = "10.1007/978-3-662-49122-5\_21",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/11060"
}
Back to top