| DUDKA, Kamil, Lukáš HOLÍK, Petr PERINGER, Marek TRTÍK and Tomáš VOJNAR. From Low-Level Pointers to High-Level Containers. In B. Jobstmann, K. Rustan, M. Leino. Verification, Model Checking, and Abstract Interpretation. LNCS, VMCAI 2016. St. Petersburg, Florida, United States: Springer, Switzerland, 2016, p. 431-452. ISBN 978-3-662-49121-8. Available from: https://dx.doi.org/10.1007/978-3-662-49122-5_21. |
Other formats:
BibTeX
LaTeX
RIS
@inproceedings{1316339,
author = {Dudka, Kamil and Holík, Lukáš and Peringer, Petr and Trtík, Marek and Vojnar, Tomáš},
address = {St. Petersburg, Florida, United States},
booktitle = {Verification, Model Checking, and Abstract Interpretation},
doi = {http://dx.doi.org/10.1007/978-3-662-49122-5_21},
edition = {LNCS, VMCAI 2016},
editor = {B. Jobstmann, K. Rustan, M. Leino},
keywords = {Shape analysis; list; program transformation},
howpublished = {tištěná verze "print"},
language = {eng},
location = {St. Petersburg, Florida, United States},
isbn = {978-3-662-49121-8},
pages = {431-452},
publisher = {Springer, Switzerland},
title = {From Low-Level Pointers to High-Level Containers},
year = {2016}
}
TY - JOUR
ID - 1316339
AU - Dudka, Kamil - Holík, Lukáš - Peringer, Petr - Trtík, Marek - Vojnar, Tomáš
PY - 2016
TI - From Low-Level Pointers to High-Level Containers
PB - Springer, Switzerland
CY - St. Petersburg, Florida, United States
SN - 9783662491218
KW - Shape analysis
KW - list
KW - program transformation
N2 - 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.
ER -
DUDKA, Kamil, Lukáš HOLÍK, Petr PERINGER, Marek TRTÍK and Tomáš VOJNAR. From Low-Level Pointers to High-Level Containers. In B. Jobstmann, K. Rustan, M. Leino. \textit{Verification, Model Checking, and Abstract Interpretation}. LNCS, VMCAI 2016. St. Petersburg, Florida, United States: Springer, Switzerland, 2016, p.~431-452. ISBN~978-3-662-49121-8. Available from: https://dx.doi.org/10.1007/978-3-662-49122-5\_{}21.
|
