{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,6]],"date-time":"2025-05-06T09:09:17Z","timestamp":1746522557202},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642388552"},{"type":"electronic","value":"9783642388569"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38856-9_10","type":"book-chapter","created":{"date-parts":[[2013,6,15]],"date-time":"2013-06-15T00:05:28Z","timestamp":1371254728000},"page":"150-171","source":"Crossref","is-referenced-by-count":8,"title":["Local Shape Analysis for Overlaid Data Structures"],"prefix":"10.1007","author":[{"given":"Cezara","family":"Dr\u0103goi","sequence":"first","affiliation":[]},{"given":"Constantin","family":"Enea","sequence":"additional","affiliation":[]},{"given":"Mihaela","family":"Sighireanu","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"10_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/3-540-45319-9_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Ball","year":"2001","unstructured":"Ball, T., Podelski, A., Rajamani, S.K.: Boolean and cartesian abstraction for model checking c programs. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 268\u2013283. Springer, Heidelberg (2001)"},{"key":"10_CR2","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":"10_CR3","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Dragoi, C., Enea, C., Sighireanu, M.: On inter-procedural analysis of programs with lists and data. In: PLDI, pp. 578\u2013589. ACM (2011)","DOI":"10.1145\/1993316.1993566"},{"key":"10_CR4","unstructured":"CEA. Frama-C Platform, \n                  \n                    http:\/\/frama-c.com"},{"key":"10_CR5","unstructured":"Celia plugin, \n                  \n                    http:\/\/www.liafa.univ-paris-diderot.fr\/celia"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Chang, B.-Y.E., Rival, X.: Relational inductive shape analysis. In: POPL, pp. 247\u2013260. ACM (2008)","DOI":"10.1145\/1328897.1328469"},{"key":"10_CR7","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":"10_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/978-3-642-22110-1_23","volume-title":"Computer Aided Verification","author":"W.-N. Chin","year":"2011","unstructured":"Chin, W.-N., Gherghina, C., Voicu, R., Le, Q.L., Craciun, F., Qin, S.: A specialization calculus for pruning disjunctive predicates to support verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 293\u2013309. Springer, Heidelberg (2011)"},{"key":"10_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/978-3-642-23217-6_16","volume-title":"CONCUR 2011 \u2013 Concurrency Theory","author":"B. Cook","year":"2011","unstructured":"Cook, B., Haase, C., Ouaknine, J., Parkinson, M.J., Worrell, J.: Tractable reasoning in a fragment of separation logic. In: Katoen, J.-P., K\u00f6nig, B. (eds.) CONCUR 2011. LNCS, vol.\u00a06901, pp. 235\u2013249. Springer, Heidelberg (2011)"},{"key":"10_CR10","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: POPL. ACM (1977)","DOI":"10.1145\/512950.512973"},{"key":"10_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/11691372_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D. Distefano","year":"2006","unstructured":"Distefano, D., O\u2019Hearn, P.W., Yang, H.: A local shape analysis based on separation logic. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 287\u2013302. Springer, Heidelberg (2006)"},{"key":"10_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"545","DOI":"10.1007\/978-3-642-28756-5_45","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Dudka","year":"2012","unstructured":"Dudka, K., M\u00fcller, P., Peringer, P., Vojnar, T.: Predator: A verification tool for programs with dynamic linked data structures - (competition contribution). In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol.\u00a07214, pp. 545\u2013548. Springer, Heidelberg (2012)"},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"Enea, C., Saveluc, V., Sighireanu, M.: Compositional invariant checking for overlaid and nested linked lists. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol.\u00a07792, pp. 129\u2013148. Springer, Heidelberg (2013)","DOI":"10.1007\/978-3-642-37036-6_9"},{"key":"10_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/11823230_16","volume-title":"Static Analysis","author":"A. Gotsman","year":"2006","unstructured":"Gotsman, A., Berdine, J., Cook, B.: Interprocedural shape analysis with separated heap abstractions. In: Yi, K. (ed.) SAS 2006. LNCS, vol.\u00a04134, pp. 240\u2013260. Springer, Heidelberg (2006)"},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Lev-Ami, T., Sagiv, M.: A combination framework for tracking partition sizes. In: POPL, pp. 239\u2013251. ACM (2009)","DOI":"10.1145\/1594834.1480912"},{"key":"10_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"592","DOI":"10.1007\/978-3-642-22110-1_48","volume-title":"Computer Aided Verification","author":"O. Lee","year":"2011","unstructured":"Lee, O., Yang, H., Petersen, R.: Program analysis for overlaid data structures. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 592\u2013608. Springer, Heidelberg (2011)"},{"key":"10_CR17","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS, pp. 55\u201374. IEEE Computer Society (2002)"},{"key":"10_CR18","doi-asserted-by":"crossref","unstructured":"Rinetzky, N., Bauer, J., Reps, T.W., Sagiv, S., Wilhelm, R.: A semantics for procedure local heaps and its abstractions. In: POPL, pp. 296\u2013309. ACM (2005)","DOI":"10.1145\/1047659.1040330"},{"key":"10_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/978-3-642-35873-9_23","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Toubhans","year":"2013","unstructured":"Toubhans, A., Chang, B.-Y.E., Rival, X.: Reduced product combination of abstract domains for shapes. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol.\u00a07737, pp. 375\u2013395. Springer, Heidelberg (2013)"},{"key":"10_CR20","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_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,14]],"date-time":"2019-05-14T00:50:28Z","timestamp":1557795028000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-38856-9_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642388552","9783642388569"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38856-9_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}