{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:08:04Z","timestamp":1776305284179,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642388552","type":"print"},{"value":"9783642388569","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38856-9_13","type":"book-chapter","created":{"date-parts":[[2013,6,15]],"date-time":"2013-06-15T04:05:28Z","timestamp":1371269128000},"page":"215-237","source":"Crossref","is-referenced-by-count":32,"title":["Byte-Precise Verification of Low-Level List Manipulation"],"prefix":"10.1007","author":[{"given":"Kamil","family":"Dudka","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Petr","family":"Peringer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tom\u00e1\u0161","family":"Vojnar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"13_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-540-73368-3_22","volume-title":"Computer Aided Verification","author":"J. Berdine","year":"2007","unstructured":"Berdine, J., Calcagno, C., Cook, B., Distefano, D., O\u2019Hearn, P.W., Wies, T., Yang, H.: Shape Analysis for Composite Data Structures. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 178\u2013192. Springer, Heidelberg (2007)"},{"key":"13_CR2","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.\u00a06806, pp. 178\u2013183. Springer, Heidelberg (2011)"},{"key":"13_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/978-3-642-31424-7_16","volume-title":"Computer Aided Verification","author":"J. Berdine","year":"2012","unstructured":"Berdine, J., Cox, A., Ishtiaq, S., Wintersteiger, C.M.: Diagnosing Abstraction Failure for Separation Logic-Based Analyses. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol.\u00a07358, pp. 155\u2013173. Springer, Heidelberg (2012)"},{"key":"13_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"594","DOI":"10.1007\/978-3-642-36742-7_43","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D. Beyer","year":"2013","unstructured":"Beyer, D.: Second competition on software verification. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol.\u00a07795, pp. 594\u2013609. Springer, Heidelberg (2013)"},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/11823230_13","volume-title":"Static Analysis","author":"C. Calcagno","year":"2006","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P.W., Yang, H.: Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic. In: Yi, K. (ed.) SAS 2006. LNCS, vol.\u00a04134, pp. 182\u2013203. Springer, Heidelberg (2006)"},{"key":"13_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"384","DOI":"10.1007\/978-3-540-74061-2_24","volume-title":"Static Analysis","author":"B.-Y.E. Chang","year":"2007","unstructured":"Chang, B.-Y.E., Rival, X., Necula, G.C.: Shape Analysis with Structural Invariant Checkers. In: Riis Nielson, H., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol.\u00a04634, pp. 384\u2013401. Springer, Heidelberg (2007)"},{"key":"13_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/978-3-642-22110-1_29","volume-title":"Computer Aided Verification","author":"K. Dudka","year":"2011","unstructured":"Dudka, K., Peringer, P., Vojnar, T.: Predator: A\u00a0Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 372\u2013378. Springer, Heidelberg (2011)"},{"key":"13_CR8","unstructured":"Dudka, K., Peringer, P., Vojnar, T.: Byte-Precise Verification of Low-Level List Manipulation. Technical report FIT-TR-2012-04, FIT BUT (2012), \n                  \n                    http:\/\/www.fit.vutbr.cz\/~idudka\/pub\/FIT-TR-2012-04.pdf"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"424","DOI":"10.1007\/978-3-642-22110-1_34","volume-title":"Computer Aided Verification","author":"P. Habermehl","year":"2011","unstructured":"Habermehl, P., Hol\u00edk, L., Rogalewicz, A., \u0160im\u00e1\u010dek, J., Vojnar, T.: Forest Automata for Verification of Heap Manipulation. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 424\u2013440. Springer, Heidelberg (2011)"},{"key":"13_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-642-11319-2_17","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"J. Kreiker","year":"2010","unstructured":"Kreiker, J., Seidl, H., Vojdani, V.: Shape Analysis of Low-Level C with Overlapping Structures. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol.\u00a05944, pp. 214\u2013230. Springer, Heidelberg (2010)"},{"key":"13_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/978-3-642-11957-6_21","volume-title":"Programming Languages and Systems","author":"V. Laviron","year":"2010","unstructured":"Laviron, V., Chang, B.-Y.E., Rival, X.: Separating Shape Graphs. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol.\u00a06012, pp. 387\u2013406. Springer, Heidelberg (2010)"},{"key":"13_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/978-3-540-78791-4_17","volume-title":"Compiler Construction","author":"M. Marron","year":"2008","unstructured":"Marron, M., Hermenegildo, M.V., Kapur, D., Stefanovic, D.: Efficient Context-Sensitive Shape Analysis with Graph Based Heap Models. In: Hendren, L. (ed.) CC 2008. LNCS, vol.\u00a04959, pp. 245\u2013259. Springer, Heidelberg (2008)"},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"Reps, T., Horwitz, S., Sagiv, M.: Precise Interprocedural Dataflow Analysis via Graph Reachability. In: Proc. of POPL 1995. ACM Press (1995)","DOI":"10.1145\/199448.199462"},{"key":"13_CR14","doi-asserted-by":"crossref","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. In: ACM Transactions on Programming Languages and Systems (TOPLAS), 24(3) (2002)","DOI":"10.1145\/514188.514190"},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"Tuch, H.: Formal Verification of C Systems Code. Journal of Automated Reasoning 42(2-4) (2009)","DOI":"10.1007\/s10817-009-9120-2"},{"key":"13_CR16","unstructured":"Yang, H., Lee, O., Calcagno, C., Distefano, D., O\u2019Hearn, P.W.: On Scalable Shape Analysis. Technical report RR-07-10, Queen Mary, University of London (2007)"},{"key":"13_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/978-3-540-70545-1_36","volume-title":"Computer Aided Verification","author":"H. Yang","year":"2008","unstructured":"Yang, H., Lee, O., Berdine, J., Calcagno, C., Cook, B., Distefano, D., O\u2019Hearn, P.W.: Scalable Shape Analysis for Systems Code. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 385\u2013398. Springer, Heidelberg (2008)"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-38856-9_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,14]],"date-time":"2019-05-14T04:50:16Z","timestamp":1557809416000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-38856-9_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642388552","9783642388569"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38856-9_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}