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.

Základní údaje

Originální název

From Low-Level Pointers to High-Level Containers

Autoři

DUDKA, Kamil (203 Česká republika), Lukáš HOLÍK (203 Česká republika), Petr PERINGER (203 Česká republika), Marek TRTÍK (203 Česká republika, domácí) a Tomáš VOJNAR (203 Česká republika, garant)

Vydání

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

Nakladatel

Springer, Switzerland

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

20206 Computer hardware and architecture

Stát vydavatele

Švýcarsko

Utajení

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

Forma vydání

tištěná verze "print"

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/16:00089165

Organizační jednotka

Fakulta informatiky

ISBN

978-3-662-49121-8

ISSN

DOI

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

UT WoS

000375148800021

Klíčová slova anglicky

Shape analysis; list; program transformation

Štítky

C language, core_B, firank_A, program transformation, shape analysis, static analysis

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 14. 5. 2020 15:18, RNDr. Pavel Šmerk, Ph.D.

Anotace

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 a 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, s. 431-452. ISBN 978-3-662-49121-8. Dostupné z: 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 a 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, s.~431-452. ISBN~978-3-662-49121-8. Dostupné z: https://dx.doi.org/10.1007/978-3-662-49122-5\_{}21.

Podrobný výpis o publikaci