{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:07:53Z","timestamp":1776305273190,"version":"3.50.1"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319667058","type":"print"},{"value":"9783319667065","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-66706-5_8","type":"book-chapter","created":{"date-parts":[[2017,8,18]],"date-time":"2017-08-18T00:13:26Z","timestamp":1503015206000},"page":"148-168","source":"Crossref","is-referenced-by-count":18,"title":["A Context-Sensitive Memory Model for Verification of C\/C++ Programs"],"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":[[2017,8,19]]},"reference":[{"key":"8_CR1","unstructured":"Data Structure Analysis (DSA) implementation. https:\/\/github.com\/seahorn\/llvm-dsa"},{"key":"8_CR2","unstructured":"SeaHorn Verification Framework. http:\/\/seahorn.github.io\/"},{"key":"8_CR3","unstructured":"Andersen, L.O.: Program analysis and specialization for the C Programming language. Technical report (1994)"},{"key":"8_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-662-53413-7_5","volume-title":"Static Analysis","author":"G Balatsouras","year":"2016","unstructured":"Balatsouras, G., Smaragdakis, Y.: Structure-sensitive points-to analysis for C and C++. In: Rival, X. (ed.) SAS 2016. LNCS, vol. 9837, pp. 84\u2013104. Springer, Heidelberg (2016). doi: 10.1007\/978-3-662-53413-7_5"},{"key":"8_CR5","unstructured":"Burstall, R.M.: Some techniques for proving correctness of programs which alter data structures. In: Machine Intelligence (1972)"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-540-71209-1_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Chatterjee","year":"2007","unstructured":"Chatterjee, S., Lahiri, S.K., Qadeer, S., Rakamari\u0107, Z.: A reachability predicate for analyzing low-level software. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 19\u201333. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-71209-1_4"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C Programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168\u2013176. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-24730-2_15"},{"key":"8_CR8","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1016\/j.entcs.2009.09.061","volume":"254","author":"E Cohen","year":"2009","unstructured":"Cohen, E., Moskal, M., Tobies, S., Schulte, W.: A precise yet efficient memory model for C. Electr. Notes Theor. Comput. Sci. 254, 85\u2013103 (2009)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Condit, J., Hackett, B., Lahiri, S.K., Qadeer, S.: Unifying type checking and property checking for low-level code. In: POPL, pp. 302\u2013314 (2009)","DOI":"10.1145\/1594834.1480921"},{"issue":"4","key":"8_CR10","doi-asserted-by":"crossref","first-page":"957","DOI":"10.1109\/TSE.2011.59","volume":"38","author":"L Cordeiro","year":"2012","unstructured":"Cordeiro, L., Fischer, B., Marques-Silva, J.: SMT-based bounded model checking for embedded ANSI-C software. IEEE Trans. Softw. Eng. 38(4), 957\u2013974 (2012)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"8_CR11","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). doi: 10.1007\/978-3-319-21690-4_20"},{"key":"8_CR12","unstructured":"Hubert, T., Marche, C.: Separation analysis for deductive verification. In: HAV (2007)"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"846","DOI":"10.1007\/978-3-642-39799-8_59","volume-title":"Computer Aided Verification","author":"A Komuravelli","year":"2013","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S., Clarke, E.M.: Automatic abstraction in SMT-based unbounded software model checking. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 846\u2013862. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39799-8_59"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Lattner, C., Adve, V.S.: LLVM: a compilation framework for lifelong program analysis & transformation. In: CGO, pp. 75\u201388 (2004)","DOI":"10.1109\/CGO.2004.1281665"},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"Lattner, C., Adve, V.S.: Automatic pool allocation: improving performance by controlling data structure layout in the heap. In: PLDI, pp. 129\u2013142 (2005)","DOI":"10.1145\/1065010.1065027"},{"key":"8_CR16","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\/1134650.1134659"},{"key":"8_CR17","unstructured":"Moy, Y.: Automatic modular static safety checking for C Programs. Ph.D. thesis, Universit\u00e9 Paris-Sud (2009)"},{"key":"8_CR18","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). doi: 10.1007\/978-3-319-08867-9_7"},{"key":"8_CR19","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). doi: 10.1007\/978-3-540-93900-9_24"},{"key":"8_CR20","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). doi: 10.1007\/978-3-540-27864-1_13"},{"key":"8_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"539","DOI":"10.1007\/978-3-319-52234-0_29","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"W Wang","year":"2017","unstructured":"Wang, W., Barrett, C., Wies, T.: Partitioned memory models for program analysis. In: Bouajjani, A., Monniaux, D. (eds.) VMCAI 2017. LNCS, vol. 10145, pp. 539\u2013558. Springer, Cham (2017). doi: 10.1007\/978-3-319-52234-0_29"},{"key":"8_CR22","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). doi: 10.1007\/978-3-642-54013-4_9"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66706-5_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,2]],"date-time":"2019-10-02T10:40:02Z","timestamp":1570012802000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66706-5_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319667058","9783319667065"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66706-5_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}