{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,14]],"date-time":"2025-07-14T02:42:34Z","timestamp":1752460954220},"publisher-location":"Berlin, Heidelberg","reference-count":37,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642253171"},{"type":"electronic","value":"9783642253188"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-25318-8_21","type":"book-chapter","created":{"date-parts":[[2011,12,3]],"date-time":"2011-12-03T21:54:45Z","timestamp":1322949285000},"page":"272-288","source":"Crossref","is-referenced-by-count":12,"title":["Soundness of Data Flow Analyses for Weak Memory Models"],"prefix":"10.1007","author":[{"given":"Jade","family":"Alglave","sequence":"first","affiliation":[]},{"given":"Daniel","family":"Kroening","sequence":"additional","affiliation":[]},{"given":"John","family":"Lugton","sequence":"additional","affiliation":[]},{"given":"Vincent","family":"Nimal","sequence":"additional","affiliation":[]},{"given":"Michael","family":"Tautschnig","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"7","key":"21_CR1","doi-asserted-by":"publisher","first-page":"779","DOI":"10.1109\/12.599898","volume":"46","author":"L. Lamport","year":"1979","unstructured":"Lamport, L.: How to Make a Correct Multiprocess Program Execute Correctly on a Multiprocessor. IEEE Trans. Comput.\u00a046(7), 779\u2013782 (1979)","journal-title":"IEEE Trans. Comput."},{"key":"21_CR2","unstructured":"Intel: Intel 64 and IA-32 Architectures Software Developer\u2019s Manual, vol.\u00a03A, rev.\u00a030. (March 2009), intel.com\/products\/processor\/manuals"},{"key":"21_CR3","unstructured":"IBM: Power ISA Version 2.06B (July 2010), power.org\/resources\/downloads\/PowerISA_V2.06B_V2_PUBLIC.pdf"},{"key":"21_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-642-14295-6_25","volume-title":"Computer Aided Verification","author":"J. Alglave","year":"2010","unstructured":"Alglave, J., Maranget, L., Sarkar, S., Sewell, P.: Fences in Weak Memory Models. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 258\u2013272. Springer, Heidelberg (2010)"},{"key":"21_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-642-19835-9_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J. Alglave","year":"2011","unstructured":"Alglave, J., Maranget, L., Sarkar, S., Sewell, P.: Litmus: Running Tests Against Hardware. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol.\u00a06605, pp. 41\u201344. Springer, Heidelberg (2011)"},{"key":"21_CR6","doi-asserted-by":"crossref","unstructured":"Manson, J., Pugh, W., Adve, S.V.: The Java Memory Model. In: POPL (2005)","DOI":"10.1145\/1040305.1040336"},{"key":"21_CR7","doi-asserted-by":"crossref","unstructured":"Boehm, H.J., Adve, S.V.: Foundations of the C++ concurrency memory model. In: PLDI (2008)","DOI":"10.1145\/1375581.1375591"},{"key":"21_CR8","doi-asserted-by":"crossref","unstructured":"Adve, S.V., Hill, M.D.: Weak ordering \u2013 A new definition. In: ISCA (1990)","DOI":"10.1145\/325164.325100"},{"key":"21_CR9","doi-asserted-by":"crossref","unstructured":"Burckhardt, S., Alur, R., Martin, M.K.: Checkfence: Checking consistency of concurrent data types on relaxed memory models. In: PLDI (2007)","DOI":"10.1145\/1250734.1250737"},{"key":"21_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-642-22110-1_6","volume-title":"Computer Aided Verification","author":"J. Alglave","year":"2011","unstructured":"Alglave, J., Maranget, L.: Stability in Weak Memory Models. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 50\u201366. Springer, Heidelberg (2011)"},{"key":"21_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-47764-0_1","volume-title":"Static Analysis","author":"M. Rinard","year":"2001","unstructured":"Rinard, M.: Analysis of Multithreaded Programs. In: Cousot, P. (ed.) SAS 2001. LNCS, vol.\u00a02126, pp. 1\u201319. Springer, Heidelberg (2001)"},{"key":"21_CR12","unstructured":"Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: International Symposium on Programming, Dunod (1976)"},{"key":"21_CR13","unstructured":"Min\u00e9, A.: The octagon abstract domain. In: Workshop on Analysis, Slicing, and Transformation (AST). IEEE (2001)"},{"key":"21_CR14","doi-asserted-by":"crossref","unstructured":"Jeannet, B.: Relational interprocedural verification of concurrent programs. In: SEFM. IEEE (2009)","DOI":"10.1109\/SEFM.2009.29"},{"key":"21_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-540-79124-9_9","volume-title":"Tests and Proofs","author":"P. Ferrara","year":"2008","unstructured":"Ferrara, P.: Static Analysis Via Abstract Interpretation of the Happens-before Memory Model. In: Beckert, B., H\u00e4hnle, R. (eds.) TAP 2008. LNCS, vol.\u00a04966, pp. 116\u2013133. Springer, Heidelberg (2008)"},{"key":"21_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1007\/978-3-642-19718-5_21","volume-title":"Programming Languages and Systems","author":"A. Min\u00e9","year":"2011","unstructured":"Min\u00e9, A.: Static Analysis of Run-Time Errors in Embedded Critical Parallel C Programs. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol.\u00a06602, pp. 398\u2013418. Springer, Heidelberg (2011)"},{"key":"21_CR17","unstructured":"Alglave, J.: A Shared Memory Poetics. PhD thesis, Universit\u00e9 Paris 7 and INRIA (2010), http:\/\/moscova.inria.fr\/~alglave\/these"},{"key":"21_CR18","doi-asserted-by":"crossref","unstructured":"Sevcik, J., Vafeiadis, V., Zappa Nardelli, F., Jagannathan, S., Sewell, P.: Relaxed-memory concurrency and verified compilation. In: POPL (2011)","DOI":"10.1145\/1926385.1926393"},{"key":"21_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-642-23702-7_14","volume-title":"Static Analysis","author":"V. Vafeiadis","year":"2011","unstructured":"Vafeiadis, V., Zappa Nardelli, F.: Verifying Fence Elimination Optimisations. In: Yahav, E. (ed.) Static Analysis. LNCS, vol.\u00a06887, pp. 146\u2013162. Springer, Heidelberg (2011)"},{"key":"21_CR20","doi-asserted-by":"crossref","unstructured":"Sewell, P., Sarkar, S., Owens, S., Zappa Nardelli, F., Myreen, M.: x86-TSO: a Rigorous and Usable Programmer\u2019s Model for x86 Multiprocessors. In: CACM (2010)","DOI":"10.1145\/1785414.1785443"},{"key":"21_CR21","unstructured":"SPARC: SPARC Architecture Manual Versions 8 and 9 (1992 and 1994), sparc.org\/standards\/V8.pdf , sparc.org\/standards\/SPARCV9.pdf"},{"key":"21_CR22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-03811-6","volume-title":"Principles of Program Analysis","author":"F. Nielson","year":"1999","unstructured":"Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer-Verlag New York, Inc., Secaucus (1999)"},{"key":"21_CR23","unstructured":"Compaq: Alpha Architecture Reference Manual, 4 edn. (2002), download.majix.org\/dec\/alpha_arch_ref.pdf"},{"key":"21_CR24","doi-asserted-by":"crossref","unstructured":"Rugina, R., Rinard, M.C.: Pointer analysis for multithreaded programs. In: PLDI (1999)","DOI":"10.1145\/301618.301645"},{"key":"21_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/978-3-642-15769-1_16","volume-title":"Static Analysis","author":"A. Farzan","year":"2010","unstructured":"Farzan, A., Kincaid, Z.: Compositional Bitvector Analysis for Concurrent Programs with Nested Locks. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol.\u00a06337, pp. 253\u2013270. Springer, Heidelberg (2010)"},{"key":"21_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/978-3-642-12002-2_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C. Wang","year":"2010","unstructured":"Wang, C., Limaye, R., Ganai, M., Gupta, A.: Trace-Based Symbolic Analysis for Atomicity Violations. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 328\u2013342. Springer, Heidelberg (2010)"},{"key":"21_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/978-3-642-05089-3_17","volume-title":"FM 2009: Formal Methods","author":"C. Wang","year":"2009","unstructured":"Wang, C., Kundu, S., Ganai, M., Gupta, A.: Symbolic Predictive Analysis for Concurrent Programs. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol.\u00a05850, pp. 256\u2013272. Springer, Heidelberg (2009)"},{"key":"21_CR28","doi-asserted-by":"crossref","unstructured":"Witkowski, T., Blanc, N., Kroening, D., Weissenbacher, G.: Model checking concurrent Linux device drivers. In: ASE. ACM (2007)","DOI":"10.1145\/1321631.1321719"},{"key":"21_CR29","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1109\/2.546611","volume":"29","author":"S.V. Adve","year":"1995","unstructured":"Adve, S.V., Gharachorloo, K.: Shared Memory Consistency Models: A Tutorial. IEEE Computer\u00a029, 66\u201376 (1995)","journal-title":"IEEE Computer"},{"key":"21_CR30","unstructured":"Adve, S., Boehm, H.J.: Memory Models: A Case for Rethinking Parallel Languages and Hardware. To appear in CACM"},{"key":"21_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/978-3-642-03359-9_27","volume-title":"Theorem Proving in Higher Order Logics","author":"S. Owens","year":"2009","unstructured":"Owens, S., Sarkar, S., Sewell, P.: A Better x86 Memory Model: x86-TSO. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 391\u2013407. Springer, Heidelberg (2009)"},{"key":"21_CR32","doi-asserted-by":"crossref","unstructured":"Callahan, D., Cooper, K.D., Kennedy, K., Torczon, L.: Interprocedural constant propagation. In: SIGPLAN Symposium on Compiler Construction (1986)","DOI":"10.1145\/12276.13327"},{"issue":"3","key":"21_CR33","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1145\/229542.229545","volume":"18","author":"J. Knoop","year":"1996","unstructured":"Knoop, J., Steffen, B., Vollmer, J.: Parallelism for free: Efficient and optimal bitvector analyses for parallel programs. ACM Trans. Program. Lang. Syst.\u00a018(3), 268\u2013299 (1996)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"21_CR34","doi-asserted-by":"crossref","unstructured":"Chugh, R., Voung, J.W., Jhala, R., Lerner, S.: Dataflow analysis for concurrent programs using datarace detection. In: Programming Language Design and Implementation (PLDI), pp. 316\u2013326. ACM (2008)","DOI":"10.1145\/1375581.1375620"},{"key":"21_CR35","doi-asserted-by":"crossref","unstructured":"Steensgaard, B.: Points-to analysis in almost linear time. In: POPL (1996)","DOI":"10.1145\/237721.237727"},{"issue":"5","key":"21_CR36","doi-asserted-by":"publisher","first-page":"1472","DOI":"10.1145\/186025.186043","volume":"16","author":"U.P. Khedker","year":"1994","unstructured":"Khedker, U.P., Dhamdhere, D.M.: A generalized theory of bit vector data flow analysis. ACM Trans. Program. Lang. Syst.\u00a016(5), 1472\u20131511 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"21_CR37","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL (1978)","DOI":"10.1145\/512760.512770"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-25318-8_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,20]],"date-time":"2019-06-20T08:01:01Z","timestamp":1561017661000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-25318-8_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642253171","9783642253188"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-25318-8_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}