From Low-Level Pointers to High-Level Containers

D 2016

From Low-Level Pointers to High-Level Containers

DUDKA, Kamil, Lukáš HOLÍK, Petr PERINGER, Marek TRTÍK, Tomáš VOJNAR et. al.

Basic information

Original name

From Low-Level Pointers to High-Level Containers

Authors

DUDKA, Kamil (203 Czech Republic), Lukáš HOLÍK (203 Czech Republic), Petr PERINGER (203 Czech Republic), Marek TRTÍK (203 Czech Republic, belonging to the institution) and Tomáš VOJNAR (203 Czech Republic, guarantor)

Edition

LNCS, VMCAI 2016. St. Petersburg, Florida, United States, Verification, Model Checking, and Abstract Interpretation, p. 431-452, 22 pp. 2016

Publisher

Springer, Switzerland

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

20206 Computer hardware and architecture

Country of publisher

Switzerland

Confidentiality degree

není předmětem státního či obchodního tajemství

Publication form

printed version "print"

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/16:00089165

Organization unit

Faculty of Informatics

ISBN

978-3-662-49121-8

ISSN

DOI

http://dx.doi.org/10.1007/978-3-662-49122-5_21

UT WoS

000375148800021

Keywords in English

Shape analysis; list; program transformation

Abstract

V originále

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.

Citovat

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.

@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.

Detailed Information on Publication Record