{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T08:30:23Z","timestamp":1770280223609,"version":"3.49.0"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030945824","type":"print"},{"value":"9783030945831","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-030-94583-1_11","type":"book-chapter","created":{"date-parts":[[2022,1,13]],"date-time":"2022-01-13T22:02:34Z","timestamp":1642111354000},"page":"219-241","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Lightweight Shape Analysis Based on\u00a0Physical Types"],"prefix":"10.1007","author":[{"given":"Olivier","family":"Nicole","sequence":"first","affiliation":[]},{"given":"Matthieu","family":"Lemerre","sequence":"additional","affiliation":[]},{"given":"Xavier","family":"Rival","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,1,14]]},"reference":[{"key":"11_CR1","unstructured":"Andersen, L.O.: Program analysis and specialization for the C programming language. Ph.D. thesis, DIKU (1994)"},{"key":"11_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., et al.: Shape analysis for composite data structures. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 178\u2013192. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73368-3_22"},{"key":"11_CR3","unstructured":"Brown, N.: Linux kernel design patterns - part 2. Linux Weekly News, June 2009"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"Chandra, S., Reps, T.: Physical type checking for C. In: ACM SIGSOFT Software Engineering Notes, vol. 24, pp. 66\u201375. ACM (1999)","DOI":"10.1145\/381788.316183"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"Chang, B.Y.E., Rival, X.: Modular construction of shape-numeric analyzers. In: Semantics, Abstract Interpretation, and Reasoning about Programs: Essays Dedicated to David A. Schmidt on the Occasion of his Sixtieth Birthday, EPTCS, vol. 129, pages 161\u2013185 (2013)","DOI":"10.4204\/EPTCS.129.26"},{"key":"11_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-YE Chang","year":"2007","unstructured":"Chang, B.-Y.E., Rival, X., Necula, G.C.: Shape analysis with structural invariant checkers. In: Nielson, H.R., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 384\u2013401. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74061-2_24"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"Cousot, P.: Types as abstract interpretations. In: Symposium on Principles of Programming Languages (POPL). ACM (1997)","DOI":"10.1145\/263699.263744"},{"key":"11_CR8","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: Symposium on Principles of Programming Languages (POPL). ACM (1977)","DOI":"10.1145\/512950.512973"},{"key":"11_CR9","doi-asserted-by":"crossref","unstructured":"Deutsch, A.: Interprocedural may-alias analysis for pointers: beyond k-limiting. In: Conference on Programming Languages Design and Implementation (PLDI), pp. 230\u2013241. ACM (1994)","DOI":"10.1145\/773473.178263"},{"key":"11_CR10","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. 3920, pp. 287\u2013302. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11691372_19"},{"key":"11_CR11","doi-asserted-by":"crossref","unstructured":"Diwan, A., McKinley, K.S., Moss, J.E.B.: Type-based alias analysis. In: Conference on Programming Languages Design and Implementation (PLDI), pp. 106\u2013117 (1998)","DOI":"10.1145\/277652.277670"},{"key":"11_CR12","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.) SAS 2013. LNCS, vol. 7935, pp. 215\u2013237. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38856-9_13"},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"Elliott, A.S., Ruef, A., Hicks, M., Tarditi, D.: Checked C: making C safe by extension. In: 2018 IEEE Cybersecurity Development (SecDev \u201918), pp. 53\u201360. IEEE, September 2018","DOI":"10.1109\/SecDev.2018.00015"},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"Freeman, T., Pfenning, F.: Refinement types for ML. In: Wise, D.S. (ed.) Proceedings of the ACM SIGPLAN\u201991 Conference on Programming Language Design and Implementation (PLDI), Toronto, Ontario, Canada, 26\u201328 June 1991, pp. 268\u2013277. ACM (1991)","DOI":"10.1145\/113446.113468"},{"key":"11_CR15","unstructured":"Jim, T., Morrisett, J.G., Grossman, D., Hicks, M.W., Cheney, J., Wang, Y.: Cyclone: a safe dialect of C. In: USENIX Annual Technical Conference, General Track, pp. 275\u2013288 (2002)"},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"Kennedy, A.: Compiling with continuations, continued. In: International Colloquium on Functional Programming (ICFP), p. 14 (2007)","DOI":"10.1145\/1291151.1291179"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"Kreiker, J., Seidl, H., Vojdani, V.: Shape analysis of low-level C with overlapping structures. In: Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), pp. 214\u2013230 (2010)","DOI":"10.1007\/978-3-642-11319-2_17"},{"key":"11_CR18","unstructured":"Lattner, C.: Macroscopic data structure analysis and optimization. Ph.D. thesis, Computer Science Dept., University of Illinois at Urbana-Champaign, Urbana, IL, May 2005. http:\/\/llvm.cs.uiuc.edu"},{"key":"11_CR19","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. 6012, pp. 387\u2013406. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-11957-6_21"},{"key":"11_CR20","doi-asserted-by":"crossref","unstructured":"Li, H., Berenger, F., Chang, B.Y.E., Rival, X.: Semantic-directed clumping of disjunctive abstract states. In: Symposium on Principles of Programming Languages (POPL), pp. 32\u201345 (2017)","DOI":"10.1145\/3093333.3009881"},{"key":"11_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1007\/978-3-662-48288-9_6","volume-title":"Static Analysis","author":"H Li","year":"2015","unstructured":"Li, H., Rival, X., Chang, B.-Y.E.: Shape analysis for unstructured sharing. In: Blazy, S., Jensen, T. (eds.) SAS 2015. LNCS, vol. 9291, pp. 90\u2013108. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-48288-9_6"},{"issue":"6","key":"11_CR22","doi-asserted-by":"publisher","first-page":"1811","DOI":"10.1145\/197320.197383","volume":"16","author":"B Liskov","year":"1994","unstructured":"Liskov, B., Wing, J.M.: A behavioral notion of subtyping. ACM Trans. Program. Lang. Syst. (TOPLAS) 16(6), 1811\u20131841 (1994)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"11_CR23","first-page":"104","volume":"47","author":"J Liu","year":"2017","unstructured":"Liu, J., Rival, X.: An array content static analysis based on non-contiguous partitions. Comput. Lang. Syst. Struct. 47, 104\u2013129 (2017)","journal-title":"Comput. Lang. Syst. Struct."},{"key":"11_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-540-27864-1_20","volume-title":"Static Analysis","author":"R Manevich","year":"2004","unstructured":"Manevich, R., Sagiv, M., Ramalingam, G., Field, J.: Partially disjunctive heap abstraction. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 265\u2013279. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27864-1_20"},{"key":"11_CR25","unstructured":"Marron, M.: Structural analysis: shape information via points-to computation. arXiv e-prints, arXiv:1201.1277 (2012)"},{"key":"11_CR26","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., Kapur, D., Stefanovic, D.: Efficient context-sensitive shape analysis with graph based heap models. In: Hendren, L. (ed.) CC 2008. LNCS, vol. 4959, pp. 245\u2013259. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78791-4_17"},{"issue":"3","key":"11_CR27","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1145\/1065887.1065892","volume":"27","author":"GC Necula","year":"2005","unstructured":"Necula, G.C., Condit, J., Harren, M., McPeak, S., Weimer, W.: CCured: type-safe retrofitting of legacy software. ACM Trans. Program. Lang. Syst. (TOPLAS) 27(3), 477\u2013526 (2005)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"11_CR28","doi-asserted-by":"crossref","unstructured":"Nicole, O., Lemerre, M., Bardin, S., Rival, X.: No crash, no exploit: automated verification of embedded kernels. In: 2021 IEEE 27th Real-Time and Embedded Technology and Applications Symposium (RTAS), pp. 27\u201339 (2021)","DOI":"10.1109\/RTAS52030.2021.00011"},{"key":"11_CR29","doi-asserted-by":"crossref","unstructured":"Nicole, O., Lemerre, M., Rival, X.: Lightweight shape analysis based on physical types (full version). Technical report, CEA List, ENS (2021). https:\/\/binsec.github.io\/assets\/publications\/papers\/2021-vmcai-full-with-appendices.pdf","DOI":"10.1007\/978-3-030-94583-1_11"},{"key":"11_CR30","unstructured":"Reynolds, J.: Separation logic: a logic for shared mutable data structures. In: Symposium on Logics In Computer Science (LICS), pp. 55\u201374. IEEE (2002)"},{"key":"11_CR31","doi-asserted-by":"crossref","unstructured":"Rondon, P.M., Kawaguchi, M., Jhala, R.: Low-level liquid types. In: Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201910), Madrid, Spain, pp. 131\u2013144. Association for Computing Machinery (2010)","DOI":"10.1145\/1706299.1706316"},{"issue":"1","key":"11_CR32","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1145\/271510.271517","volume":"20","author":"M Sagiv","year":"1998","unstructured":"Sagiv, M., Reps, T., Whilhelm, R.: Solving shape-analysis problems in languages with destructive updating. ACM Trans. Program. Lang. Syst. (TOPLAS) 20(1), 50 (1998)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"issue":"3","key":"11_CR33","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"M Sagiv","year":"2002","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst. (TOPLAS) 24(3), 217\u2013298 (2002)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"issue":"1","key":"11_CR34","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1561\/2500000014","volume":"2","author":"Y Smaragdakis","year":"2015","unstructured":"Smaragdakis, Y., Balatsouras, G.: Pointer analysis. FNT in programming languages 2(1), 1\u201369 (2015)","journal-title":"FNT in programming languages"},{"key":"11_CR35","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/62.2160","volume":"31","author":"RE Tarjan","year":"1984","unstructured":"Tarjan, R.E., van Leeuwen, J.: Worst-case analysis of set union algorithms. JACM 31, 245\u2013281 (1984)","journal-title":"JACM"},{"key":"11_CR36","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. 7737, pp. 375\u2013395. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-35873-9_23"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-94583-1_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,14]],"date-time":"2022-01-14T00:04:46Z","timestamp":1642118686000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-94583-1_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030945824","9783030945831"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-94583-1_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"14 January 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Philadelphia, PA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 January 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 January 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vmcai2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/popl22.sigplan.org\/home\/VMCAI-2022","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"63","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"23","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"37% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}