{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,25]],"date-time":"2026-02-25T18:42:59Z","timestamp":1772044979560,"version":"3.50.1"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319522333","type":"print"},{"value":"9783319522340","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-52234-0_29","type":"book-chapter","created":{"date-parts":[[2017,1,10]],"date-time":"2017-01-10T23:52:06Z","timestamp":1484092326000},"page":"539-558","source":"Crossref","is-referenced-by-count":14,"title":["Partitioned Memory Models for Program Analysis"],"prefix":"10.1007","author":[{"given":"Wei","family":"Wang","sequence":"first","affiliation":[]},{"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[]},{"given":"Thomas","family":"Wies","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,1,12]]},"reference":[{"key":"29_CR1","unstructured":"Andersen, L.O.: Program analysis and specialization for the C programming language. Ph.D. thesis, University of Copenhagen, May 1994"},{"key":"29_CR2","doi-asserted-by":"crossref","unstructured":"Balatsouras, G., Smaragdakis, Y.: Structure-sensitive points-to analysis for C and C++. In: Static Analysis Symposium (SAS) (2016)","DOI":"10.1007\/978-3-662-53413-7_5"},{"key":"29_CR3","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard - version 2.0. In: Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (SMT) (2010)"},{"key":"29_CR4","doi-asserted-by":"crossref","unstructured":"Beyer, D.: Reliable and reproducible competition results with benchexec and witnesses (reported on SV-COMP 2016). In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (2016)","DOI":"10.1007\/978-3-662-49674-9_55"},{"key":"29_CR5","doi-asserted-by":"crossref","unstructured":"B\u00f6hme, S., Moskal, M.: Heaps, data structures: a challenge for automated provers. In: Conference on Automated Deduction (CADE) (2011)","DOI":"10.1007\/978-3-642-22438-6_15"},{"key":"29_CR6","first-page":"23","volume":"7","author":"RM Burstall","year":"1972","unstructured":"Burstall, R.M.: Some techniques for proving correctness of programs which alter data structures. Mach. Intell. 7, 23\u201350 (1972)","journal-title":"Mach. Intell."},{"key":"29_CR7","doi-asserted-by":"crossref","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (2004)","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"29_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. Electron. Notes Theor. Comput. Sci. (ENTCS) 254, 85\u2013103 (2009)","journal-title":"Electron. Notes Theor. Comput. Sci. (ENTCS)"},{"key":"29_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: Principles of Programming Languages (POPL) (2009)","DOI":"10.1145\/1594834.1480921"},{"key":"29_CR10","doi-asserted-by":"crossref","unstructured":"Conway, C.L., Dams, D., Namjoshi, K.S., Barrett, C.: Pointer analysis, conditional soundness, and proving the absence of errors. In: Static Analysis Symposium (SAS) (2008)","DOI":"10.1007\/978-3-540-69166-2_5"},{"key":"29_CR11","doi-asserted-by":"crossref","unstructured":"Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C a software analysis perspective. In: Software Engineering and Formal Methods (SEFM) (2012)","DOI":"10.1007\/978-3-642-33826-7_16"},{"key":"29_CR12","unstructured":"Foster, J.S., F\u00e4hndrich, M., Aiken, A.: Flow-insensitive points-to analysis with term and set constraints. Technical report CSD-97-964, University of California, Berkeley (1997)"},{"key":"29_CR13","doi-asserted-by":"crossref","unstructured":"Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: Computer Aided Verification (CAV) (2015)","DOI":"10.1007\/978-3-319-21690-4_20"},{"key":"29_CR14","doi-asserted-by":"crossref","unstructured":"Hind, M.: Pointer analysis: haven\u2019t we solved this problem yet? In: Program Analysis for Software Tools and Engineering (PASTE) (2001)","DOI":"10.1145\/379605.379665"},{"key":"29_CR15","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Qadeer, S.: Back to the future: revisiting precise program verification using SMT solvers. In: Principles of Programming Languages (POPL) (2008)","DOI":"10.1145\/1328438.1328461"},{"key":"29_CR16","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Qadeer, S., Rakamari\u0107, Z.: Static and precise detection of concurrency errors in systems code using SMT solvers. In: Computer Aided Verification (CAV) (2009)","DOI":"10.1007\/978-3-642-02658-4_38"},{"key":"29_CR17","doi-asserted-by":"crossref","unstructured":"Lal, A., Qadeer, S.: Powering the static driver verifier using Corral. In: Foundations of Software Engineering (FSE) (2014)","DOI":"10.1145\/2635868.2635894"},{"key":"29_CR18","doi-asserted-by":"crossref","unstructured":"Lattner, C., Lenharth, A., Adve, V.: Making context-sensitive points-to analysis with heap cloning practical for the real world. In: Programming Language Design and Implementation (PLDI) (2007)","DOI":"10.1145\/1250734.1250766"},{"key":"29_CR19","doi-asserted-by":"crossref","unstructured":"Min\u00e9, A.: Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics. In: Language, Compilers, and Tool Support for Embedded Systems (LCTES) (2006)","DOI":"10.1145\/1134650.1134659"},{"key":"29_CR20","doi-asserted-by":"crossref","unstructured":"Morse, J., Ramalho, M., Cordeiro, L., Nicole, D., Fischer, B.: ESBMC 1.22 (competition contribution). In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (2014)","DOI":"10.1007\/978-3-642-54862-8_31"},{"key":"29_CR21","doi-asserted-by":"crossref","unstructured":"Necula, G.C., McPeak, S., Weimer, W.: CCured: type-safe retrofitting of legacy code. In: Principles of Programming Languages (POPL) (2002)","DOI":"10.1145\/503272.503286"},{"key":"29_CR22","doi-asserted-by":"crossref","unstructured":"Pearce, D.J., Kelly, P.H.J., Hankin, C.: Efficient field-sensitive pointer analysis for C. In: Program Analysis for Software Tools and Engineering (PASTE) (2004)","DOI":"10.1145\/996821.996835"},{"issue":"1","key":"29_CR23","doi-asserted-by":"crossref","first-page":"4","DOI":"10.1145\/1290520.1290524","volume":"30","author":"DJ Pearce","year":"2007","unstructured":"Pearce, D.J., Kelly, P.H.J., Hankin, C.: Efficient field-sensitive pointer analysis of C. ACM Trans. Program. Lang. Syst. 30(1), 4 (2007)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"29_CR24","doi-asserted-by":"crossref","unstructured":"Rakamari\u0107, Z., Emmi, M.: SMACK: decoupling source language details from verifier implementations. In: Computer Aided Verification (CAV) (2015)","DOI":"10.1007\/978-3-319-08867-9_7"},{"key":"29_CR25","doi-asserted-by":"crossref","unstructured":"Rakamari\u0107, Z., Hu, A.J.: A scalable memory model for low-level code. In: Verification, Model Checking, and Abstract Interpretation (VMCAI) (2009)","DOI":"10.1007\/978-3-540-93900-9_24"},{"key":"29_CR26","doi-asserted-by":"crossref","unstructured":"Steensgaard, B.: Points-to analysis by type inference of programs with structures and unions. In: Compiler Construction (CC) (1996)","DOI":"10.1007\/3-540-61053-7_58"},{"key":"29_CR27","doi-asserted-by":"crossref","unstructured":"Steensgaard, B.: Points-to analysis in almost linear time. In: Principles of Programming Languages (POPL) (1996)","DOI":"10.1145\/237721.237727"},{"key":"29_CR28","unstructured":"Wang, W.: Partition memory models for program analysis. Ph.D. thesis, New York University, May 2016"},{"key":"29_CR29","doi-asserted-by":"crossref","unstructured":"Wang, W., Barrett, C., Wies, T.: Cascade 2.0. In: Verification, Model Checking, and Abstract Interpretation (VMCAI) (2014)","DOI":"10.1007\/978-3-642-54013-4_9"},{"key":"29_CR30","doi-asserted-by":"crossref","unstructured":"Yong, S.H., Horwitz, S., Reps, T.: Pointer analysis for programs with structures and casting. In: Programming Language Design and Implementation (PLDI) (1999)","DOI":"10.1145\/301618.301647"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-52234-0_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,17]],"date-time":"2019-09-17T07:10:05Z","timestamp":1568704205000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-52234-0_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319522333","9783319522340"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-52234-0_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}