{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T04:14:01Z","timestamp":1748751241145,"version":"3.41.0"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662491218"},{"type":"electronic","value":"9783662491225"}],"license":[{"start":{"date-parts":[[2015,12,25]],"date-time":"2015-12-25T00:00:00Z","timestamp":1451001600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-662-49122-5_21","type":"book-chapter","created":{"date-parts":[[2015,12,24]],"date-time":"2015-12-24T05:01:36Z","timestamp":1450933296000},"page":"431-452","source":"Crossref","is-referenced-by-count":1,"title":["From Low-Level Pointers to High-Level Containers"],"prefix":"10.1007","author":[{"given":"Kamil","family":"Dudka","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luk\u00e1\u0161","family":"Hol\u00edk","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Petr","family":"Peringer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marek","family":"Trt\u00edk","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tom\u00e1\u0161","family":"Vojnar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,12,25]]},"reference":[{"key":"21_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-642-22110-1_15","volume-title":"Computer Aided Verification","author":"J Berdine","year":"2011","unstructured":"Berdine, J., Cook, B., Ishtiaq, S.: SLAyer: memory safety for systems-level code. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 178\u2013183. Springer, Heidelberg (2011)"},{"key":"21_CR2","doi-asserted-by":"crossref","unstructured":"Chilimbi, T.M., Hill, M.D., Larus, J.R.: Cache-conscious structure layout. In: Proceedings of PLDI 1999, pp. 1\u201312. ACM (1999)","DOI":"10.1145\/301631.301633"},{"key":"21_CR3","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of POPL 1977, pp. 238\u2013252. ACM (1977)","DOI":"10.1145\/512950.512973"},{"key":"21_CR4","unstructured":"Cozzie, A., Stratton, F., Xue, H., King, S.T.: Digging for data structures. In: Proceedings of USENIX 2008, pp. 255\u2013266. USENIX Association (2008)"},{"key":"21_CR5","doi-asserted-by":"crossref","unstructured":"Dekker, R., Ververs, F.: Abstract data structure recognition. In: Proceedings of KBSE 1994, pp. 133\u2013140 (1994)","DOI":"10.1109\/KBSE.1994.342669"},{"key":"21_CR6","doi-asserted-by":"crossref","unstructured":"Demsky, B., Ernst, M.D., Guo, P.J., McCamant, S., Perkins, J.H., Rinard, M.C.: Inference and enforcement of data structure consistency specifications. In: Proceedings of ISSTA 2006, pp. 233\u2013244. ACM (2006)","DOI":"10.1145\/1146238.1146266"},{"key":"21_CR7","first-page":"431","volume-title":"Lecture Notes in Computer Science","author":"Kamil Dudka","year":"2015","unstructured":"Dudka, K., Hol\u00edk, L., Peringer, P., Trt\u00edk, M., Vojnar, T.: From low-level pointers to high-level containers. Technical report FIT-TR-2015-03 arXiv:1510.07995 , FIT BUT (2015). http:\/\/arxiv.org\/abs\/1510.07995"},{"key":"21_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/978-3-642-38856-9_13","volume-title":"Static Analysis","author":"K Dudka","year":"2013","unstructured":"Dudka, K., Peringer, P., Vojnar, T.: Byte-precise verification of low-level list manipulation. In: Logozzo, F., F\u00e4hndrich, M. (eds.) Static Analysis. LNCS, vol. 7935, pp. 215\u2013237. Springer, Heidelberg (2013)"},{"issue":"1","key":"21_CR9","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/s10703-012-0150-8","volume":"41","author":"P Habermehl","year":"2012","unstructured":"Habermehl, P., Hol\u00edk, L., Rogalewicz, A., Sim\u00e1cek, J., Vojnar, T.: Forest automata for verification of heap manipulation. Formal Meth. Syst. Des. 41(1), 83\u2013106 (2012)","journal-title":"Formal Meth. Syst. Des."},{"key":"21_CR10","doi-asserted-by":"crossref","unstructured":"Haller, I., Slowinska, A., Bos, H.: MemPick: high-level data structure detection in C\/C++ binaries. In: Proceedings of WCRE 2013, pp. 32\u201341 (2013)","DOI":"10.1109\/WCRE.2013.6671327"},{"issue":"1","key":"21_CR11","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1109\/71.80123","volume":"1","author":"LJ Hendren","year":"1990","unstructured":"Hendren, L.J., Nicolau, A.: Parallelizing programs with recursive data structures. IEEE Trans. Parallel Distrib. Syst. 1(1), 35\u201347 (1990)","journal-title":"IEEE Trans. Parallel Distrib. Syst."},{"key":"21_CR12","doi-asserted-by":"crossref","unstructured":"Jump, M., McKinley, K.S.: Dynamic shape analysis via degree metrics. In: Proceedings of ISMM 2009, pp. 119\u2013128. ACM (2009)","DOI":"10.1145\/1542431.1542449"},{"key":"21_CR13","doi-asserted-by":"crossref","unstructured":"Jung, C., Clark, N.: DDT: design and evaluation of a dynamic program analysis for optimizing data structure usage. In: Proceedings of MICRO 2009, pp. 56\u201366. ACM (2009)","DOI":"10.1145\/1669112.1669122"},{"key":"21_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44802-0_1","volume-title":"Computer Science Logic","author":"PW O\u2019Hearn","year":"2001","unstructured":"O\u2019Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, pp. 1\u201319. Springer, Heidelberg (2001)"},{"key":"21_CR15","unstructured":"Par\u00edzek, P.: J2BP. http:\/\/plg.uwaterloo.ca\/~pparizek\/j2bp"},{"issue":"10","key":"21_CR16","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1145\/2398857.2384623","volume":"47","author":"Pavel Par\u00edzek","year":"2012","unstructured":"Par\u00edzek, P., Lhot\u00e1k, O.: Predicate abstraction of java programs with collections. In: Proceedings of OOPSLA 2012, pp. 75\u201394. ACM (2012)","journal-title":"ACM SIGPLAN Notices"},{"key":"21_CR17","doi-asserted-by":"crossref","unstructured":"Pheng, S., Verbrugge, C.: Dynamic data structure analysis for java programs. In: Proceedings of ICPC 2006, pp. 191\u2013201. IEEE Computer Society (2006)","DOI":"10.1109\/ICPC.2006.20"},{"key":"21_CR18","doi-asserted-by":"crossref","unstructured":"Raman, E., August, D.I.: Recursive data structure profiling. In: Proceedings of MSP 2005, pp. 5\u201314. ACM (2005)","DOI":"10.1145\/1111583.1111585"},{"key":"21_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-00590-9_25","volume-title":"Programming Languages and Systems","author":"M Raza","year":"2009","unstructured":"Raza, M., Calcagno, C., Gardner, P.: Automatic parallelization with separation logic. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 348\u2013362. Springer, Heidelberg (2009)"},{"issue":"3","key":"21_CR20","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"S Sagiv","year":"2002","unstructured":"Sagiv, S., Reps, T.W., Wilhelm, R.: Parametric shape analysis via 3-valued logic. TOPLAS 24(3), 217\u2013298 (2002)","journal-title":"TOPLAS"},{"key":"21_CR21","doi-asserted-by":"crossref","unstructured":"Shaham, R., Kolodner, E.K., Sagiv, S.: On the Effectiveness of GC in Java. In: Proceedings of ISMM 2000, pp. 12\u201317. ACM (2000)","DOI":"10.1145\/362426.362430"},{"key":"21_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/978-3-642-11319-2_25","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"V Vafeiadis","year":"2010","unstructured":"Vafeiadis, V.: RGSep action inference. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 345\u2013361. Springer, Heidelberg (2010)"},{"key":"21_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-642-36742-7_25","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"DH White","year":"2013","unstructured":"White, D.H., L\u00fcttgen, G.: Identifying dynamic data structures by learning evolving patterns in memory. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 354\u2013369. Springer, Heidelberg (2013)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49122-5_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T22:49:43Z","timestamp":1748731783000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49122-5_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,12,25]]},"ISBN":["9783662491218","9783662491225"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49122-5_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015,12,25]]}}}