{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T13:02:44Z","timestamp":1760101364908,"version":"3.40.3"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030955601"},{"type":"electronic","value":"9783030955618"}],"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-95561-8_8","type":"book-chapter","created":{"date-parts":[[2022,2,21]],"date-time":"2022-02-21T19:04:21Z","timestamp":1645470261000},"page":"122-144","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":14,"title":["Abstract Interpretation of\u00a0LLVM with\u00a0a\u00a0Region-Based Memory Model"],"prefix":"10.1007","author":[{"given":"Arie","family":"Gurfinkel","sequence":"first","affiliation":[]},{"given":"Jorge A.","family":"Navas","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,2,22]]},"reference":[{"key":"8_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/11823230_15","volume-title":"Static Analysis","author":"G Balakrishnan","year":"2006","unstructured":"Balakrishnan, G., Reps, T.: Recency-abstraction for heap-allocated storage. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 221\u2013239. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11823230_15"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Blanchet, B., et al.: A static analyzer for large safety-critical software. In: PLDI, pp. 196\u2013207 (2003)","DOI":"10.1145\/780822.781153"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-319-52234-0_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S Blazy","year":"2017","unstructured":"Blazy, S., B\u00fchler, D., Yakobowski, B.: Structuring abstract interpreters through state and value abstractions. In: Bouajjani, A., Monniaux, D. (eds.) VMCAI 2017. LNCS, vol. 10145, pp. 112\u2013130. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-52234-0_7"},{"key":"8_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-030-11245-5_8","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"Q Bouillaguet","year":"2019","unstructured":"Bouillaguet, Q., Bobot, F., Sighireanu, M., Yakobowski, B.: Exploiting pointer analysis in memory models for deductive verification. In: Enea, C., Piskac, R. (eds.) VMCAI 2019. LNCS, vol. 11388, pp. 160\u2013182. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-11245-5_8"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/978-3-319-10431-7_20","volume-title":"Software Engineering and Formal Methods","author":"G Brat","year":"2014","unstructured":"Brat, G., Navas, J.A., Shi, N., Venet, A.: IKOS: a framework for static analysis based on abstract interpretation. In: Giannakopoulou, D., Sala\u00fcn, G. (eds.) SEFM 2014. LNCS, vol. 8702, pp. 271\u2013277. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10431-7_20"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/978-3-642-20398-5_33","volume-title":"NASA Formal Methods","author":"C Calcagno","year":"2011","unstructured":"Calcagno, C., Distefano, D.: Infer: an automatic program verifier for memory safety of C programs. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 459\u2013465. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-20398-5_33"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/3-540-61053-7_66","volume-title":"Compiler Construction","author":"F Chow","year":"1996","unstructured":"Chow, F., Chan, S., Liu, S.-M., Lo, R., Streich, M.: Effective representation of aliases and indirect memory operations in SSA form. In: Gyim\u00f3thy, T. (ed.) CC 1996. LNCS, vol. 1060, pp. 253\u2013267. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61053-7_66"},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/978-3-540-69166-2_5","volume-title":"Static Analysis","author":"CL Conway","year":"2008","unstructured":"Conway, C.L., Dams, D., Namjoshi, K.S., Barrett, C.: Pointer analysis, conditional soundness, and proving the absence of errors. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol. 5079, pp. 62\u201377. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-69166-2_5"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-17822-6_1","volume-title":"Logic-Based Program Synthesis and Transformation","author":"JRM Cornish","year":"2015","unstructured":"Cornish, J.R.M., Gange, G., Navas, J.A., Schachte, P., S\u00f8ndergaard, H., Stuckey, P.J.: Analyzing array manipulating programs by program transformation. In: Proietti, M., Seki, H. (eds.) LOPSTR 2014. LNCS, vol. 8981, pp. 3\u201320. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-17822-6_1"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-642-33826-7_16","volume-title":"Software Engineering and Formal Methods","author":"P Cuoq","year":"2012","unstructured":"Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 233\u2013247. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33826-7_16"},{"key":"8_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-540-30482-1_10","volume-title":"Formal Methods and Software Engineering","author":"J-C Filli\u00e2tre","year":"2004","unstructured":"Filli\u00e2tre, J.-C., March\u00e9, C.: Multi-prover verification of C programs. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 15\u201329. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30482-1_10"},{"key":"8_CR12","unstructured":"Gopan, D.: Numeric program analysis techniques with applications to array analysis and library summarization. Ph.D. thesis, University of Wisconsin (2007)"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-319-21690-4_20","volume-title":"Computer Aided Verification","author":"A Gurfinkel","year":"2015","unstructured":"Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 343\u2013361. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_20"},{"key":"8_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-319-66706-5_8","volume-title":"Static Analysis","author":"A Gurfinkel","year":"2017","unstructured":"Gurfinkel, A., Navas, J.A.: A context-sensitive memory model for verification of C\/C++ programs. In: Ranzato, F. (ed.) SAS 2017. LNCS, vol. 10422, pp. 148\u2013168. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66706-5_8"},{"key":"8_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/978-3-319-57288-8_15","volume-title":"NASA Formal Methods","author":"H Illous","year":"2017","unstructured":"Illous, H., Lemerre, M., Rival, X.: A relational shape abstract domain. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 212\u2013229. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-57288-8_15"},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"Jourdan, J., Laporte, V., Blazy, S., Leroy, X., Pichardie, D.: A formally-verified C static analyzer. In: POPL, pp. 247\u2013259 (2015)","DOI":"10.1145\/2775051.2676966"},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-030-41600-3_1","volume-title":"Verified Software. Theories, Tools, and Experiments","author":"M Journault","year":"2020","unstructured":"Journault, M., Min\u00e9, A., Monat, R., Ouadjaout, A.: Combinations of reusable abstract domains for a multilingual static analyzer. In: Chakraborty, S., Navas, J.A. (eds.) VSTTE 2019. LNCS, vol. 12031, pp. 1\u201318. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-41600-3_1"},{"key":"8_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-319-99725-4_16","volume-title":"Static Analysis","author":"M Journault","year":"2018","unstructured":"Journault, M., Min\u00e9, A., Ouadjaout, A.: Modular static analysis of string manipulations in C programs. In: Podelski, A. (ed.) SAS 2018. LNCS, vol. 11002, pp. 243\u2013262. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-99725-4_16"},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"Kuderski, J., Navas, J.A., Gurfinkel, A.: Unification-based pointer analysis without oversharing. In: FMCAD, pp. 37\u201345 (2019)","DOI":"10.23919\/FMCAD.2019.8894275"},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"Min\u00e9, A.: Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics. In: LCTES, pp. 54\u201363 (2006)","DOI":"10.1145\/1159974.1134659"},{"key":"8_CR21","unstructured":"Moy, Y.: Automatic modular static safety checking for C programs. Ph.D. thesis, Universit\u00e9 Paris-Sud (2009)"},{"key":"8_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1007\/978-3-319-08867-9_7","volume-title":"Computer Aided Verification","author":"Z Rakamari\u0107","year":"2014","unstructured":"Rakamari\u0107, Z., Emmi, M.: SMACK: decoupling source language details from verifier implementations. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 106\u2013113. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_7"},{"key":"8_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/978-3-540-93900-9_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"Z Rakamari\u0107","year":"2008","unstructured":"Rakamari\u0107, Z., Hu, A.J.: A scalable memory model for low-level code. In: Jones, N.D., M\u00fcller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 290\u2013304. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-93900-9_24"},{"key":"8_CR24","doi-asserted-by":"crossref","unstructured":"Sui, Y., Xue, J.: SVF: interprocedural static value-flow analysis in LLVM. In: CC, pp. 265\u2013266 (2016)","DOI":"10.1145\/2892208.2892235"},{"key":"8_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-540-27864-1_13","volume-title":"Static Analysis","author":"A Venet","year":"2004","unstructured":"Venet, A.: A scalable nonuniform pointer analysis for embedded programs. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 149\u2013164. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27864-1_13"},{"key":"8_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/978-3-642-54013-4_9","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"W Wang","year":"2014","unstructured":"Wang, W., Barrett, C., Wies, T.: Cascade 2.0. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 142\u2013160. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54013-4_9"},{"key":"8_CR27","unstructured":"Warren, R., Hermenegildo, M.V., Debray, S.K.: On the practicality of global flow analysis of logic programs. In: ICLP, pp. 684\u2013699 (1988)"}],"container-title":["Lecture Notes in Computer Science","Software Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-95561-8_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,2,21]],"date-time":"2022-02-21T19:05:04Z","timestamp":1645470304000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-95561-8_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030955601","9783030955618"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-95561-8_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"22 February 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VSTTE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Working Conference on Verified Software: Theories, Tools, and Experiments","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 October 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 October 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vstte2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/verify.inf.usi.ch\/VSTTE21","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":"17","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":"7","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":"41% - 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,1","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":"2,3","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)"}}]}}