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. |
Další formáty:
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 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.
|